From 00608fac2d8e217232d5f2ddd28a43971bf259b7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 31 Mar 2003 21:18:53 +0000
Subject: Ajout d'un message à FailTac

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 translate/pptacticnew.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'translate')

diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index b80ae29d65..99c4bee7d9 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 ->
-- 
cgit v1.2.3