From 466c25ea43149deedf50e0105a6d1e69db91c8fd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 4 Sep 2014 17:58:12 +0200
Subject: Removing the old implementation of clear_body.

---
 tactics/tactics.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6800ca71ed..e006404eba 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
-- 
cgit v1.2.3