From 08d457e14bef86d80447ab3c6de387e1a95ec29a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 14 Nov 2003 22:46:37 +0000
Subject: Move des hyps de NewInduction: retour a situation V7.4 a defaut
 d'etre robuste

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4916 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ee8e32d0aa..145b86bdc2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1128,10 +1128,10 @@ let induct_discharge statuslists destopt avoid' (avoid,ra) names gl =
         check_unused_names names;
         tclIDTAC gl
   in
-  let intros_move lstatus gl =
+  let intros_move lstatus =
     let newlstatus = (* if some IH has taken place at the top of hyps *)
       List.map (function (hyp,None) -> (hyp,!tophyp) | x -> x) lstatus in
-    intros_move newlstatus gl
+    intros_move newlstatus
   in 
   tclTHENLIST [ peel_tac ra names;
 		intros_rmove rstatus;
-- 
cgit v1.2.3