aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/refiner.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/refiner.mli')
-rw-r--r--proofs/refiner.mli6
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