diff options
| author | herbelin | 2006-01-21 11:18:36 +0000 |
|---|---|---|
| committer | herbelin | 2006-01-21 11:18:36 +0000 |
| commit | 642e522429e6f5faa381aaf26cd530a939b5a601 (patch) | |
| tree | b3621f545e4bcdd4cc98ba32511d646f99a99844 /parsing | |
| parent | 8f967888479a614eac56d30bde49a4dad9178740 (diff) | |
Messages de idtac et fail peuvent maintenant être des listes de string, int et variables ltac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7911 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 2 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 11 |
2 files changed, 10 insertions, 3 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 54d68bbea6..80dcf23e32 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -35,7 +35,7 @@ GEXTEND Gram ; command: [ [ IDENT "Goal"; c = Constr.lconstr -> VernacGoal c - | IDENT "Proof" -> VernacProof (Tacexpr.TacId "") + | IDENT "Proof" -> VernacProof (Tacexpr.TacId []) | IDENT "Proof"; "with"; ta = tactic -> VernacProof ta | IDENT "Abort" -> VernacAbort None | IDENT "Abort"; IDENT "All" -> VernacAbortAll diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index fcd21098df..e4bc4549bc 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -247,6 +247,11 @@ let mlexpr_of_match_rule f = function | Tacexpr.Pat (l,mp,t) -> <:expr< Tacexpr.Pat $mlexpr_of_list mlexpr_of_match_context_hyps l$ $mlexpr_of_match_pattern mp$ $f t$ >> | Tacexpr.All t -> <:expr< Tacexpr.All $f t$ >> +let mlexpr_of_message_token = function + | Tacexpr.MsgString s -> <:expr< Tacexpr.MsgString $str:s$ >> + | Tacexpr.MsgInt n -> <:expr< Tacexpr.MsgInt $mlexpr_of_int n$ >> + | Tacexpr.MsgIdent id -> <:expr< Tacexpr.MsgIdent $mlexpr_of_hyp id$ >> + let rec mlexpr_of_atomic_tactic = function (* Basic tactics *) | Tacexpr.TacIntroPattern pl -> @@ -405,8 +410,10 @@ 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 s -> <:expr< Tacexpr.TacId $str:s$ >> - | Tacexpr.TacFail (n,s) -> <:expr< Tacexpr.TacFail $mlexpr_of_or_var mlexpr_of_int n$ $str:s$ >> + | Tacexpr.TacId l -> + <:expr< Tacexpr.TacId $mlexpr_of_list mlexpr_of_message_token l$ >> + | Tacexpr.TacFail (n,l) -> + <:expr< Tacexpr.TacFail $mlexpr_of_or_var mlexpr_of_int n$ $mlexpr_of_list mlexpr_of_message_token l$ >> (* | Tacexpr.TacInfo t -> TacInfo (loc,f t) |