From 442febce538255a19467e98ba8b46a43726ea98c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 23 Dec 2003 20:00:46 +0000
Subject: Reparation semantique casse de Pose en v7

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5138 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 translate/pptacticnew.ml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 8dd636c296..e0c8331ffb 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -494,8 +494,17 @@ and pr_atom1 env = function
              hov 1 (str"(" ++ pr_name na ++ str " :=" ++
                     pr_lconstrarg env c ++ str")"))
   | TacForward (true,Anonymous,c) ->
-      hov 1 (str "pose" ++ pr_constrarg env c)
+      if Options.do_translate () then
+        (* Pose was buggy and was wrongly substituting in conclusion in v7 *)
+        hov 1 (str "set" ++ pr_constrarg env c)
+      else
+        hov 1 (str "pose" ++ pr_constrarg env c)
   | TacForward (true,Name id,c) ->
+      if Options.do_translate () then
+      hov 1 (str "set" ++ spc() ++
+             hov 1 (str"(" ++ pr_id id ++ str " :=" ++
+                    pr_lconstrarg env c ++ str")"))
+      else
       hov 1 (str "pose" ++ spc() ++
              hov 1 (str"(" ++ pr_id id ++ str " :=" ++
                     pr_lconstrarg env c ++ str")"))
-- 
cgit v1.2.3