diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-15 14:03:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-15 14:07:13 +0200 |
| commit | aae3c3b42a9bad20ebde4a139e6de660fbb8e042 (patch) | |
| tree | 188895bdaa3835f6175406fb0d22e282441448a5 /proofs/refiner.mli | |
| parent | c69404402212ed9d541899ae78ac889e62cf238a (diff) | |
Removing unused Refiner.tclWITHHOLES.
Diffstat (limited to 'proofs/refiner.mli')
| -rw-r--r-- | proofs/refiner.mli | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 171b008d1..58f9b9617 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -138,9 +138,3 @@ val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic (* 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 - extension of the sigma of the goal *) -val tclWITHHOLES : bool -> ('a -> tactic) -> evar_map -> 'a -> tactic |