From 359398d061e7639867dd14c5af6b640027e8bcb8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 7 Apr 2003 08:35:59 +0000
Subject: Aérer les := et : de "assert"

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

diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 99c4bee7d9..38cbc3109f 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -260,13 +260,13 @@ and pr_atom1 env = function
       hov 1 (str "assert" ++ pr_lconstrarg env c)
   | TacTrueCut (Some id,c) -> 
       hov 1 (str "assert" ++ spc () ++ pr_id id ++ str ":" ++
-             pr_lconstr env c)
+             pr_lconstrarg env c)
   | TacForward (false,na,c) ->
-      hov 1 (str "assert" ++ pr_arg pr_name na ++ str ":=" ++
-             pr_lconstr env c)
+      hov 1 (str "assert" ++ pr_arg pr_name na ++ str " :=" ++
+             pr_lconstrarg env c)
   | TacForward (true,na,c) ->
-      hov 1 (str "pose" ++ pr_arg pr_name na ++ str ":=" ++
-             pr_lconstr env c)
+      hov 1 (str "pose" ++ pr_arg pr_name na ++ str " :=" ++
+             pr_lconstrarg env c)
   | TacGeneralize l ->
       hov 1 (str "generalize" ++ spc () ++
              prlist_with_sep spc (pr_constr env) l)
@@ -274,8 +274,8 @@ and pr_atom1 env = function
       hov 1 (str "generalize" ++ spc () ++ str "dependent" ++
              pr_lconstrarg env c)
   | TacLetTac (id,c,cl) ->
-      hov 1 (str "lettac" ++ spc () ++ pr_id id ++ str ":=" ++
-        pr_constr env c ++ pr_clause_pattern pr_ident cl)
+      hov 1 (str "lettac" ++ spc () ++ pr_id id ++ str " :=" ++
+        pr_constrarg env c ++ pr_clause_pattern pr_ident cl)
   | TacInstantiate (n,c) ->
       hov 1 (str "instantiate" ++ pr_arg int n ++ pr_lconstrarg env c)
 
-- 
cgit v1.2.3