From ca2bca80347b0983e9a0b420360121ef82d72c71 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 2 May 2006 14:54:14 +0000
Subject: Correction bug du correctif bug assert as

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

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0c05792959..0314c960ca 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1078,9 +1078,12 @@ let letin_tac with_eq name c occs gl =
   
 (* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *)
 let forward usetac ipat c gl =
-  let tac = match usetac with None -> exact_no_check c | Some tac -> tac in
-  let t = refresh_universes (pf_type_of gl c) in
-  tclTHENFIRST (assert_as true ipat t) tac gl
+  match usetac with
+  | None -> 
+      let t = refresh_universes (pf_type_of gl c) in
+      tclTHENFIRST (assert_as true ipat t) (exact_no_check c) gl
+  | Some tac -> 
+      tclTHENFIRST (assert_as true ipat c) tac gl
 
 (*****************************)
 (* High-level induction      *)
-- 
cgit v1.2.3