Removing the old implementation of clear_body.

5 files changed, 0 insertions, 48 deletions

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