Removing the old implementation of clear_body.

8 files changed, 2 insertions, 54 deletions

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 8f20cea6b..b5566127f 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -222,7 +222,7 @@ let add_justification_hyps keep items gls =
 	  let id=pf_get_new_id local_hyp_prefix gls in
 	    keep:=Id.Set.add id !keep;
 	    tclTHEN (Proofview.V82.of_tactic (letin_tac None (Names.Name id) c None Locusops.nowhere))
-              (thin_body [id]) gls in
+              (Proofview.V82.of_tactic (clear_body [id])) gls in
     tclMAP add_aux items gls
 
 let prepare_goal items gls =
diff --git a/printing/printer.ml b/printing/printer.ml
index 8c7dbac33..f105e8031 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -663,9 +663,6 @@ let pr_prim_rule = function
   | Thin ids ->
       (str"clear "  ++ pr_sequence pr_id ids)
 
-  | ThinBody ids ->
-      (str"clearbody "  ++ pr_sequence pr_id ids)
-
   | Move (withdep,id1,id2) ->
       (str (if withdep then "dependent " else "") ++
 	 str"move "  ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index a7538193b..b9cff0527 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -113,35 +113,6 @@ let clear_hyps2 sigma ids sign t cl =
 
 (* The ClearBody tactic *)
 
-let recheck_typability (what,id) env sigma t =
-  try check_typability env sigma t
-  with e when Errors.noncritical e ->
-    let s = match what with
-      | None -> "the conclusion"
-      | Some id -> "hypothesis "^(Id.to_string id) in
-    error
-      ("The correctness of "^s^" relies on the body of "^(Id.to_string id))
-
-let remove_hyp_body env sigma id =
-  let sign =
-    apply_to_hyp_and_dependent_on (named_context_val env) id
-      (fun (_,c,t) _ ->
-	match c with
-	| None -> error ((Id.to_string id)^" is not a local definition.")
-	| Some c ->(id,None,t))
-      (fun (id',c,t as d) sign ->
-	(if !check then
-	  begin
-	    let env = reset_with_named_context sign env in
-	    match c with
-	    | None ->  recheck_typability (Some id',id) env sigma t
-	    | Some b ->
-		let b' = mkCast (b,DEFAULTcast, t) in
-		recheck_typability (Some id',id) env sigma b'
-	  end;d))
-  in
-  reset_with_named_context sign env
-
 (* Reordering of the context *)
 
 (* faire le minimum d'echanges pour que l'ordre donne soit un *)
@@ -708,17 +679,6 @@ let prim_refiner r sigma goal =
 	let sigma = Goal.V82.partial_solution sigma goal ev in
 	  ([gl], sigma)
 
-    | ThinBody ids ->
-	let clear_aux env id =
-          let env' = remove_hyp_body env sigma id in
-            if !check then recheck_typability (None,id) env' sigma cl;
-            env'
-	in
-	let sign' = named_context_val (List.fold_left clear_aux env ids) in
-     	let (sg,ev,sigma) = mk_goal sign' cl in
-	let sigma = Goal.V82.partial_solution sigma goal ev in
-     	  ([sg], sigma)
-
     | Move (withdep, hfrom, hto) ->
   	let (left,right,declfrom,toleft) =
 	  split_sign hfrom hto (named_context_of_val sign) in
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 7297706e1..76459a59a 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -35,7 +35,6 @@ type prim_rule =
   | Convert_concl of types * cast_kind
   | Convert_hyp of named_declaration
   | Thin of Id.t list
-  | ThinBody of Id.t list
   | Move of bool * Id.t * Id.t move_location
   | Rename of Id.t * Id.t
 
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 0aadd862b..bbb2c8e09 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -27,7 +27,6 @@ type prim_rule =
   | Convert_concl of types * cast_kind
   | Convert_hyp of named_declaration
   | Thin of Id.t list
-  | ThinBody of Id.t list
   | Move of bool * Id.t * Id.t move_location
   | Rename of Id.t * Id.t
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index f87d03183..6c72009d4 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -127,10 +127,6 @@ let convert_hyp_no_check d gl =
 let thin_no_check ids gl =
   if List.is_empty ids then tclIDTAC gl else refiner (Thin ids) gl
 
-(* This does not check dependencies *)
-let thin_body_no_check ids gl =
-  if List.is_empty ids then tclIDTAC gl else refiner (ThinBody ids) gl
-
 let move_hyp_no_check with_dep id1 id2 gl =
   refiner (Move (with_dep,id1,id2)) gl
 
@@ -155,7 +151,6 @@ let refine c           = with_check (refine_no_check c)
 let convert_concl d sty = with_check (convert_concl_no_check d sty)
 let convert_hyp d      = with_check (convert_hyp_no_check d)
 let thin c             = with_check (thin_no_check c)
-let thin_body c        = with_check (thin_body_no_check c)
 let move_hyp b id id'  = with_check (move_hyp_no_check b id id')
 let rename_hyp l       = with_check (rename_hyp_no_check l)
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index c7729e416..cebe78ed0 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -100,7 +100,6 @@ val refine           : constr -> tactic
 val convert_concl    : types -> cast_kind -> tactic
 val convert_hyp      : named_declaration -> tactic
 val thin             : Id.t list -> tactic
-val thin_body        : Id.t list -> tactic
 val move_hyp         : bool -> Id.t -> Id.t move_location -> tactic
 val rename_hyp       : (Id.t*Id.t) list -> tactic
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6800ca71e..e006404eb 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -138,7 +138,6 @@ let introduction    = Tacmach.introduction
 let refine          = Tacmach.refine
 let convert_concl   = Tacmach.convert_concl
 let convert_hyp     = Tacmach.convert_hyp
-let thin_body       = Tacmach.thin_body
 
 let convert_gen pb x y =
   Proofview.Goal.raw_enter begin fun gl ->
@@ -2009,7 +2008,7 @@ let letin_tac_gen with_eq abs ty =
             sigma, term,
             Tacticals.New.tclTHEN
 	      (intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false)
-	      (Proofview.V82.tactic (thin_body [heq;id]))
+	      (clear_body [heq;id])
       | None ->
 	  (Proofview.Goal.sigma gl, mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) in
     Tacticals.New.tclTHEN