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_eautoSource
Source
val esearch :
bool ->
int ->
Tactypes.delayed_open_constr list ->
Hints.hint_db list ->
Pp.t list ->
Pp.t list ->
Backtracking.trace Proofview.tacticSearches a sequence of at most n tactics within db_list and lems that solves the goal
The goal can contain evars
Source
val wp_eauto :
bool ->
int ->
Tactypes.delayed_open_constr list ->
string list ->
Backtracking.trace Proofview.tacticWaterproof eauto
This function is a rewrite around Eauto.eauto with the same arguments to be able to retrieve which hints have been used in case of success.
The code structure has been rearranged to match the one of wp_auto.wp_auto.
Source
val rwp_eauto :
bool ->
int ->
Tactypes.delayed_open_constr list ->
Hints.hint_db_name list ->
Pp.t list ->
Pp.t list ->
Backtracking.trace Proofview.tacticRestricted Waterproof eauto
This function acts the same as wp_auto but will fail if all proof found contain at least one must-use lemma that is unused or one hint that is in the forbidden list.