diff options
| author | narboux | 2003-11-12 18:03:50 +0000 |
|---|---|---|
| committer | narboux | 2003-11-12 18:03:50 +0000 |
| commit | ecf5fbd6bc5fc12166dd36c1b12ec714b86d0a63 (patch) | |
| tree | 2c9927b2d22c456dd07daddff5cc56cabdfb8b2d /parsing | |
| parent | ea9f6b8f620b9f69de9d72ca603af042e4487339 (diff) | |
Idtac peut prendre un argument à afficher
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4863 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_ltac.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_ltacnew.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_proofs.ml4 | 2 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 5 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 2 |
5 files changed, 7 insertions, 6 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 41ee54ea42..51480a9560 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -166,7 +166,7 @@ GEXTEND Gram TacFirst l | IDENT "Solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> TacSolve l - | IDENT "Idtac" -> TacId + | IDENT "Idtac" ; s = [ s = STRING -> s | -> ""] -> TacId s | IDENT "Fail"; n = [ n = natural -> n | -> fail_default_value ]; s = [ s = STRING -> s | -> ""] -> TacFail (n,s) | st = simple_tactic -> TacAtom (loc,st) diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4 index aaf31da534..1f02415261 100644 --- a/parsing/g_ltacnew.ml4 +++ b/parsing/g_ltacnew.ml4 @@ -110,7 +110,7 @@ GEXTEND Gram TacFirst l | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> TacSolve l - | IDENT "idtac" -> TacId + | IDENT "idtac"; s = [ s = STRING -> s | -> ""] -> TacId s | IDENT "fail"; n = [ n = natural -> n | -> fail_default_value ]; s = [ s = STRING -> s | -> ""] -> TacFail (n,s) | st = simple_tactic -> TacAtom (loc,st) diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index c462c3bdc0..638591460c 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -36,7 +36,7 @@ GEXTEND Gram ; command: [ [ IDENT "Goal"; c = Constr.constr -> VernacGoal c - | "Proof" -> VernacProof Tacexpr.TacId + | "Proof" -> VernacProof (Tacexpr.TacId "") | "Proof"; "with"; ta = tactic -> VernacProof ta | IDENT "Abort" -> VernacAbort None | IDENT "Abort"; IDENT "All" -> VernacAbortAll diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index ea5ad236e7..4397f67695 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -565,7 +565,7 @@ and pr_tactic_seq_body tl = 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" + | TacId "" -> str "Idtac" | TacFail (0,"") -> str "Fail" | TacAtom (_,t) -> pr_atom0 t | TacArg c -> pr_tacarg c @@ -574,6 +574,7 @@ and pr0 = function (* Semi-closed atomic tactic expressions *) and pr1 = function | TacAtom (_,t) -> pr_atom1 t + | TacId s -> str "Idtac \"" ++ str s ++ str "\"" | 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 "\"" @@ -619,7 +620,7 @@ and pr6 = function | TacDo _ | TacRepeat _ | TacProgress _ - | TacId + | TacId _ | TacFail _ | TacInfo _) as t -> pr5 t diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 01be09fc68..dfe341beb8 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -470,7 +470,7 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function <:expr< Tacexpr.TacRepeat $mlexpr_of_tactic t$ >> | Tacexpr.TacProgress t -> <:expr< Tacexpr.TacProgress $mlexpr_of_tactic t$ >> - | Tacexpr.TacId -> <:expr< Tacexpr.TacId >> + | Tacexpr.TacId s -> <:expr< Tacexpr.TacId $str:s$ >> | Tacexpr.TacFail (n,s) -> <:expr< Tacexpr.TacFail $int:string_of_int n$ $str:s$ >> (* | Tacexpr.TacInfo t -> TacInfo (loc,f t) |