diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-07 08:35:59 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-07 08:35:59 +0000 |
| commit | 359398d061e7639867dd14c5af6b640027e8bcb8 (patch) | |
| tree | 8e0a0c4de45789de5d7a2468f1207b11e854a1bc /translate | |
| parent | 7f9203aa720dd16fa151d08d626124488c211994 (diff) | |
Aérer les := et : de "assert"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3851 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/pptacticnew.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index 99c4bee7d..38cbc3109 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) |