From 140aa7e12c0735b7c3e793436378bf015b5c6dec Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 2 May 2006 09:38:21 +0000
Subject: Bug assert as

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

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cb735fb057..0c05792959 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1078,12 +1078,9 @@ let letin_tac with_eq name c occs gl =
   
 (* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *)
 let forward usetac ipat c gl =
-  match usetac with
-  | None -> 
-      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
+  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
 
 (*****************************)
 (* High-level induction      *)
-- 
cgit v1.2.3