Correction sur commit précédent : Tactics.cut réduisait de manière inappropriée

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5409 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 4 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cebc6697e..6444c1756 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -506,19 +506,20 @@ let cut_and_apply c gl =
 (*     Cut tactics        *)
 (**************************)
 
-let true_cut na c gl =
+let assert_tac first na c gl =
   match kind_of_term (hnf_type_of gl c) with
     | Sort s -> 
-	let id =
-	  match na with
+	let id = match na with
 	  | Anonymous -> 
               let d = match s with Prop _ -> "H" | Type _ -> "X" in
               fresh_id [] (id_of_string d) gl
 	  | Name id -> id
 	in
-	internal_cut id c gl
+	(if first then internal_cut else internal_cut_rev) id c gl
     | _  -> error "Not a proposition or a type"
 
+let true_cut = assert_tac true
+
 let cut c gl =
   match kind_of_term (hnf_type_of gl c) with
     | Sort _ ->