diff options
Diffstat (limited to 'proofs/refiner.mli')
| -rw-r--r-- | proofs/refiner.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/proofs/refiner.mli b/proofs/refiner.mli index c198958e3..8fc9e9e17 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -121,7 +121,6 @@ val tclAT_LEAST_ONCE : tactic -> tactic val tclFAIL : int -> Pp.std_ppcmds -> tactic val tclFAIL_lazy : int -> Pp.std_ppcmds Lazy.t -> tactic val tclDO : int -> tactic -> tactic -val tclTIMEOUT : int -> tactic -> tactic val tclWEAK_PROGRESS : tactic -> tactic val tclPROGRESS : tactic -> tactic val tclSHOWHYPS : tactic -> tactic @@ -152,6 +151,11 @@ val then_tactic_list : tactic_list -> tactic_list -> tactic_list val tactic_list_tactic : tactic_list -> tactic val goal_goal_list : 'a sigma -> 'a list sigma + +(* Check that holes in arguments have been resolved *) +(* spiwack: used in [tclWITHHOLES] both newer and older copy. *) +val check_evars : Environ.env -> evar_map -> evar_map -> evar_map -> unit + (** [tclWITHHOLES solve_holes tac (sigma,c)] applies [tac] to [c] which may have unresolved holes; if [solve_holes] these holes must be resolved after application of the tactic; [sigma] must be an |