diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-02 09:12:24 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-02 09:12:24 +0000 |
| commit | 26d73ca5440e45d7832935876fa8acdea6277df5 (patch) | |
| tree | e95502c3043044a9c501726dee9d0ea73760b86c /translate | |
| parent | 1fee844708da1de1144cb17b0289938d709a6593 (diff) | |
Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation dans ltac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5418 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/pptacticnew.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index e5e3a1fa0..cbe659063 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -704,7 +704,7 @@ let rec pr_tac env inherited tac = hov 1 (str "try" ++ spc () ++ pr_tac env (ltactical,E) t), ltactical | TacDo (n,t) -> - hov 1 (str "do " ++ int n ++ spc () ++ pr_tac env (ltactical,E) t), + hov 1 (str "do " ++ pr_or_var int n ++ spc () ++ pr_tac env (ltactical,E) t), ltactical | TacRepeat t -> hov 1 (str "repeat" ++ spc () ++ pr_tac env (ltactical,E) t), @@ -719,9 +719,9 @@ let rec pr_tac env inherited tac = hov 1 (pr_tac env (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++ pr_tac env (lorelse,E) t2), lorelse - | TacFail (0,"") -> str "fail", latom + | TacFail (ArgArg 0,"") -> str "fail", latom | TacFail (n,s) -> - str "fail" ++ (if n=0 then mt () else pr_arg int n) ++ + str "fail" ++ (if n=ArgArg 0 then mt () else pr_arg (pr_or_var int) n) ++ (if s="" then mt() else qsnew s), latom | TacFirst tl -> str "first" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet |