Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Page
Library
Module
Module type
Parameter
Class
Class type
Source
package coq-waterproof
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Module Waterproof.Wp_bulletsSource
This module registers two new bullet behaviors available for use in Waterproof. With
Set Bullet Behavior "Waterproof Strict Subproofs".
one basically gets the default bullet behavior, with slightly different suggestion and error messages.
With
Set Bullet Behavior "Waterproof Relaxed Subproofs".
it doesn't matter which exact bullets one uses in a particular place: they all function the same.