diff options
| author | Arnaud Spiwack | 2014-12-19 10:28:58 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-12-19 16:27:45 +0100 |
| commit | fb9815baafc008a6e67e542eb8c2adf7a6375fe8 (patch) | |
| tree | 206244b9fb02320c8ab6b7c0381e9da4eaeb19b5 /grammar | |
| parent | a07648ca9c6b06414b271632c620122e51bf0f4a (diff) | |
Add a backtracking version of Ltac's [match].
[multimatch … with …] returns every possible successes: every matching branch and every successes of these matching branch, so that subsequent tactics can backtrack as well.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/q_coqast.ml4 | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index 1a11b00282..e3d910f321 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -289,6 +289,11 @@ let mlexpr_of_pattern_ast = mlexpr_of_constr let mlexpr_of_entry_type = function _ -> failwith "mlexpr_of_entry_type: TODO" +let mlexpr_of_match_lazy_flag = function + | Tacexpr.General -> <:expr<Tacexpr.General>> + | Tacexpr.Lazy -> <:expr<Tacexpr.Lazy>> + | Tacexpr.Once -> <:expr<Tacexpr.Once>> + let mlexpr_of_match_pattern = function | Tacexpr.Term t -> <:expr< Tacexpr.Term $mlexpr_of_pattern_ast t$ >> | Tacexpr.Subterm (b,ido,t) -> @@ -479,12 +484,12 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function <:expr< Tacexpr.TacLetIn $mlexpr_of_bool isrec$ $mlexpr_of_list f l$ $mlexpr_of_tactic t$ >> | Tacexpr.TacMatch (lz,t,l) -> <:expr< Tacexpr.TacMatch - $mlexpr_of_bool lz$ + $mlexpr_of_match_lazy_flag lz$ $mlexpr_of_tactic t$ $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>> | Tacexpr.TacMatchGoal (lz,lr,l) -> <:expr< Tacexpr.TacMatchGoal - $mlexpr_of_bool lz$ + $mlexpr_of_match_lazy_flag lz$ $mlexpr_of_bool lr$ $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>> |