Put the "clear" tactic into the monad.

4 files changed, 0 insertions, 18 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 09f308abef..df5a12473b 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -636,16 +636,6 @@ let prim_refiner r sigma goal =
 	let sigma = Goal.V82.partial_solution sigma goal oterm in
 	  (sgl, sigma)
 
-    (* And now the structural rules *)
-    | Thin ids ->
-        let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in
-	let (hyps,concl,nsigma) = clear_hyps env sigma ids sign cl in
-	let (gl,ev,sigma) =
-	  Goal.V82.mk_goal nsigma hyps concl (Goal.V82.extra nsigma goal)
-	in
-	let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
-	  ([gl], sigma)
-
     | Move (hfrom, hto) ->
   	let (left,right,declfrom,toleft) =
 	  split_sign hfrom hto (named_context_of_val sign) in
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index b4c9dae2a3..48ad50c7a0 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -22,7 +22,6 @@ type prim_rule =
   | FixRule of Id.t * int * (Id.t * int * constr) list * int
   | Cofix of Id.t * (Id.t * constr) list * int
   | Refine of constr
-  | Thin of Id.t list
   | Move of Id.t * Id.t move_location
 
 (** Nowadays, the only rules we'll consider are the primitive rules *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 33cef7486b..67daccb81d 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -121,10 +121,6 @@ let internal_cut_rev_no_check replace id t gl =
 let refine_no_check c gl =
   refiner (Refine c) gl
 
-(* This does not check dependencies *)
-let thin_no_check ids gl =
-  if List.is_empty ids then tclIDTAC gl else refiner (Thin ids) gl
-
 let move_hyp_no_check id1 id2 gl =
   refiner (Move (id1,id2)) gl
 
@@ -139,7 +135,6 @@ let mutual_cofix f others j gl =
 let internal_cut b d t = with_check (internal_cut_no_check b d t)
 let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t)
 let refine c           = with_check (refine_no_check c)
-let thin c             = with_check (thin_no_check c)
 let move_hyp id id'  = with_check (move_hyp_no_check id id')
 
 (* Pretty-printers *)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index f786b5f218..fef205f823 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -86,7 +86,6 @@ val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
 val refiner                   : rule -> tactic
 val internal_cut_no_check     : bool -> Id.t -> types -> tactic
 val refine_no_check           : constr -> tactic
-val thin_no_check             : Id.t list -> tactic
 val mutual_fix      :
   Id.t -> int -> (Id.t * int * constr) list -> int -> tactic
 val mutual_cofix    : Id.t -> (Id.t * constr) list -> int -> tactic
@@ -96,7 +95,6 @@ val mutual_cofix    : Id.t -> (Id.t * constr) list -> int -> tactic
 val internal_cut     : bool -> Id.t -> types -> tactic
 val internal_cut_rev : bool -> Id.t -> types -> tactic
 val refine           : constr -> tactic
-val thin             : Id.t list -> tactic
 val move_hyp         : Id.t -> Id.t move_location -> tactic
 
 (** {6 Pretty-printing functions (debug only). } *)