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 /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/g_ltac.ml4 | 4 | ||||
| -rw-r--r-- | parsing/g_ltacnew.ml4 | 4 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 6 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 2 |
4 files changed, 9 insertions, 7 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 7519df465..d05827bfe 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -189,8 +189,8 @@ GEXTEND Gram | IDENT "Solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> TacSolve l | IDENT "Idtac" -> TacId - | IDENT "Fail" -> TacFail fail_default_value - | IDENT "Fail"; n = natural -> TacFail n + | IDENT "Fail"; n = [ n = natural -> n | -> fail_default_value ]; + s = [ s = STRING -> s | -> ""] -> TacFail (n,s) | st = simple_tactic -> TacAtom (loc,st) | "("; a = tactic_expr; ")" -> a | a = tactic_arg -> TacArg a diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4 index dc78f5faa..2caad4680 100644 --- a/parsing/g_ltacnew.ml4 +++ b/parsing/g_ltacnew.ml4 @@ -110,8 +110,8 @@ GEXTEND Gram | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> TacSolve l | IDENT "idtac" -> TacId - | IDENT "fail" -> TacFail fail_default_value - | IDENT "fail"; n = natural -> TacFail n + | IDENT "fail"; n = [ n = natural -> n | -> fail_default_value ]; + s = [ s = STRING -> s | -> ""] -> TacFail (n,s) | st = simple_tactic -> TacAtom (loc,st) | IDENT "eval"; rtc = red_expr; "in"; c = Constr.lconstr -> TacArg(ConstrMayEval (ConstrEval (rtc,c))) diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index fbeb697eb..c67ce496d 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -489,7 +489,7 @@ and pr0 = function | TacFirst tl -> str "First" ++ spc () ++ pr_tactic_seq_body tl | TacSolve tl -> str "Solve" ++ spc () ++ pr_tactic_seq_body tl | TacId -> str "Idtac" - | TacFail 0 -> str "Fail" + | TacFail (0,"") -> str "Fail" | TacAtom (_,t) -> pr_atom0 t | TacArg c -> pr_tacarg c | t -> str "(" ++ prtac t ++ str ")" @@ -497,7 +497,9 @@ and pr0 = function (* Semi-closed atomic tactic expressions *) and pr1 = function | TacAtom (_,t) -> pr_atom1 t - | TacFail n -> str "Fail " ++ int n + | TacFail (0,s) -> str "Fail \"" ++ str s ++ str "\"" + | TacFail (n,"") -> str "Fail " ++ int n + | TacFail (n,s) -> str "Fail " ++ int n ++ str "\"" ++ str s ++ str "\"" | t -> pr0 t (* Orelse tactic expressions (printed as if parsed associating on the right diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 2b3967707..dd1ce4ec2 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -471,7 +471,7 @@ and mlexpr_of_tactic = function | Tacexpr.TacProgress t -> <:expr< Tacexpr.TacProgress $mlexpr_of_tactic t$ >> | Tacexpr.TacId -> <:expr< Tacexpr.TacId >> - | Tacexpr.TacFail n -> <:expr< Tacexpr.TacFail $int:string_of_int n$ >> + | Tacexpr.TacFail (n,s) -> <:expr< Tacexpr.TacFail $int:string_of_int n$ $str:s$ >> (* | Tacexpr.TacInfo t -> TacInfo (loc,f t) |