From 26d73ca5440e45d7832935876fa8acdea6277df5 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 2 Mar 2004 09:12:24 +0000 Subject: Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation dans ltac MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5418 85f007b7-540e-0410-9357-904b9bb8a0f7 --- translate/pptacticnew.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'translate/pptacticnew.ml') 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 -- cgit v1.2.3