From 44d42fe1cf68c042fdcacacfe1b9c6eb7e62773b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 21 Jan 2006 11:02:20 +0000
Subject: Backtrack commit précédent (incompatible avec le choix de prendre
 Idtac comme défaut pour ne rien faire)

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

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7d7c4e3190..f57b490fc4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1080,7 +1080,7 @@ let forward usetac ipat c gl =
       let t = refresh_universes (pf_type_of gl c) in
       tclTHENS (assert_as true ipat t) [exact_no_check c; tclIDTAC] gl
   | Some tac -> 
-      tclTHENS (assert_as true ipat c) [tclCOMPLETE tac; tclIDTAC] gl
+      tclTHENS (assert_as true ipat c) [tac; tclIDTAC] gl
 
 (*****************************)
 (* High-level induction      *)
-- 
cgit v1.2.3