1 files changed, 3 insertions, 60 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 353d35f6a2..932bfc5fe7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -138,6 +138,7 @@ 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 ->
@@ -1466,65 +1467,7 @@ let assumption =
 let clear ids = (* avant seul dyn_clear n'echouait pas en [] *)
   if List.is_empty ids then tclIDTAC else thin ids
 
-let on_the_bodies = function
-| [] -> assert false
-| [id] -> str " depends on the body of " ++ pr_id id
-| l -> str " depends on the bodies of " ++ pr_sequence pr_id l
-
-let check_is_type env ty msg =
-  Proofview.tclEVARMAP >>= fun sigma ->
-  let evdref = ref sigma in
-  try
-    let _ = Typing.sort_of env evdref ty in
-    Proofview.V82.tclEVARS !evdref
-  with e when Errors.noncritical e ->
-    msg e
-
-let clear_body ids =
-  Proofview.Goal.raw_enter begin fun gl ->
-    let env = Proofview.Goal.env gl in
-    let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
-    let ctx = named_context env in
-    let map (id, body, t as decl) = match body with
-    | None ->
-      let () = if List.mem_f Id.equal id ids then
-        errorlabstrm "" (str "Hypothesis " ++ pr_id id ++ str " is not a local definition")
-      in
-      decl
-    | Some _ ->
-      if List.mem_f Id.equal id ids then (id, None, t) else decl
-    in
-    let ctx = List.map map ctx in
-    let filter = function
-    | (id, None, _) -> Some (mkVar id)
-    | _ -> None
-    in
-    let base_env = reset_context env in
-    let env = push_named_context ctx base_env in
-    let check_hyps =
-      let check env (id, _, t as decl) =
-        let msg _ = Tacticals.New.tclZEROMSG
-          (str "Hypothesis " ++ pr_id id ++ on_the_bodies ids)
-        in
-        check_is_type env t msg <*> Proofview.tclUNIT (push_named decl env)
-      in
-      let checks = Proofview.Monad.List.fold_left check base_env (List.rev ctx) in
-      Proofview.tclIGNORE checks
-    in
-    let check_concl =
-      let msg _ = Tacticals.New.tclZEROMSG
-        (str "Conclusion" ++ on_the_bodies ids)
-      in
-      check_is_type env concl msg
-    in
-    check_hyps <*> check_concl <*>
-    Proofview.Refine.refine ~unsafe:true begin fun h ->
-      let args = Array.of_list (List.map_filter filter ctx) in
-      let (h, c) = Proofview.Refine.new_evar h env concl in
-      let c = it_mkNamedLambda_or_LetIn c ctx in
-      (h, mkApp (c, args))
-    end
-  end
+let clear_body = thin_body
 
 let clear_wildcards ids =
   Proofview.V82.tactic (tclMAP (fun (loc,id) gl ->
@@ -2015,7 +1958,7 @@ let letin_tac_gen with_eq abs ty =
             sigma, term,
             Tacticals.New.tclTHEN
 	      (intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false)
-	      (clear_body [heq;id])
+	      (Proofview.V82.tactic (thin_body [heq;id]))
       | None ->
 	  (Proofview.Goal.sigma gl, mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) in
     Tacticals.New.tclTHEN