diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-31 21:18:53 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-31 21:18:53 +0000 |
| commit | 00608fac2d8e217232d5f2ddd28a43971bf259b7 (patch) | |
| tree | 0bd65009594d83c85a6e3f4f5bf8a0e77e0b4fc6 /translate/pptacticnew.ml | |
| parent | ca29570a25be8f9b8757399f5f0b72b4a9bd5e43 (diff) | |
Ajout d'un message à FailTac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate/pptacticnew.ml')
| -rw-r--r-- | translate/pptacticnew.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index b80ae29d6..99c4bee7d 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -281,15 +281,15 @@ and pr_atom1 env = function (* Derived basic tactics *) | TacOldInduction h -> - hov 1 (str "induction" ++ pr_arg pr_quantified_hypothesis h) + hov 1 (str "oldinduction" ++ pr_arg pr_quantified_hypothesis h) | TacNewInduction (h,e,ids) -> - hov 1 (str "newinduction" ++ spc () ++ + hov 1 (str "induction" ++ spc () ++ pr_induction_arg (pr_lconstr env) h ++ pr_opt (pr_eliminator env) e ++ pr_with_names ids) | TacOldDestruct h -> - hov 1 (str "destruct" ++ pr_arg pr_quantified_hypothesis h) + hov 1 (str "olddestruct" ++ pr_arg pr_quantified_hypothesis h) | TacNewDestruct (h,e,ids) -> - hov 1 (str "newdestruct" ++ spc () ++ + hov 1 (str "destruct" ++ spc () ++ pr_induction_arg (pr_lconstr env) h ++ pr_opt (pr_eliminator env) e ++ pr_with_names ids) | TacDoubleInduction (h1,h2) -> @@ -462,8 +462,10 @@ 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 n -> str "fail " ++ int n, latom + | TacFail (0,"") -> str "fail", latom + | TacFail (n,s) -> + str "fail" ++ (if n=0 then mt () else pr_arg int n) ++ + (if s="" then mt() else str " \"" ++ str s ++ str "\""), latom | TacFirst tl -> str "first" ++ spc () ++ pr_seq_body (pr_tac env) tl, llet | TacSolve tl -> |