From a5f8a0b25a6f610d3323913b4e4307cf0dc393ff Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 20 Jan 2006 22:30:38 +0000
Subject: Ajout de la contrainte de résoudre l'assertion dans 'assert by'

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

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f57b490fc4..7d7c4e3190 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) [tac; tclIDTAC] gl
+      tclTHENS (assert_as true ipat c) [tclCOMPLETE tac; tclIDTAC] gl
 
 (*****************************)
 (* High-level induction      *)
-- 
cgit v1.2.3