diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-09 19:02:58 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-09 19:02:58 +0000 |
| commit | b1bd8f2a50863a6ca77b6f05b3f1756648cfe936 (patch) | |
| tree | f9ab63c12f45c28bcc9320712e401c6ef32f26a1 /translate/pptacticnew.ml | |
| parent | c4bc84f02c7d22402824514d70c6d5e66f511bfc (diff) | |
bugs avec Pose et Assert
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5190 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate/pptacticnew.ml')
| -rw-r--r-- | translate/pptacticnew.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index a6ff11b0e..5e0cc68ba 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -483,9 +483,9 @@ and pr_atom1 env = function hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++ str"with " ++ prlist_with_sep spc (pr_cofix_tac env) l) | TacCut c -> hov 1 (str "cut" ++ pr_constrarg env c) - | TacTrueCut (None,c) -> + | TacTrueCut (Anonymous,c) -> hov 1 (str "assert" ++ pr_constrarg env c) - | TacTrueCut (Some id,c) -> + | TacTrueCut (Name id,c) -> hov 1 (str "assert" ++ spc () ++ hov 1 (str"(" ++ pr_id id ++ str " :" ++ pr_lconstrarg env c ++ str")")) @@ -495,7 +495,7 @@ and pr_atom1 env = function pr_lconstrarg env c ++ str")")) | TacForward (true,Anonymous,c) -> if Options.do_translate () then - (* Pose was buggy and was wrongly substituting in conclusion in v7 *) + (* Pose was buggy and was wrongly substituted in conclusion in v7 *) hov 1 (str "set" ++ pr_constrarg env c) else hov 1 (str "pose" ++ pr_constrarg env c) @@ -514,7 +514,9 @@ and pr_atom1 env = function | TacGeneralizeDep c -> hov 1 (str "generalize" ++ spc () ++ str "dependent" ++ pr_constrarg env c) - | TacLetTac (id,c,cl) -> + | TacLetTac (Anonymous,c,cl) -> + hov 1 (str "set" ++ pr_constrarg env c) ++ pr_clauses pr_ident cl + | TacLetTac (Name id,c,cl) -> hov 1 (str "set" ++ spc () ++ hov 1 (str"(" ++ pr_id id ++ str " :=" ++ pr_lconstrarg env c ++ str")") ++ |