diff options
| author | Théo Zimmermann | 2019-06-19 10:41:09 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-06-19 10:41:09 +0200 |
| commit | cdba5f7ceee1adfbdd96ffc82115fbc1e6750b80 (patch) | |
| tree | e4e94c235b18bdf96b82db071da74535ccd827c5 /plugins/ltac/tacarg.ml | |
| parent | 415e83efb9e767ddf65b8c27d4e497592fd61f2c (diff) | |
| parent | 459b5ce5b2b825db43d645357f83d7fe17289bc5 (diff) | |
Merge PR #10239: Deprecate grammar entry "intropattern" in tactic notations in favor of "simple_intropattern"
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/ltac/tacarg.ml')
| -rw-r--r-- | plugins/ltac/tacarg.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml index c9dbbea1ea..9e8e86d4fc 100644 --- a/plugins/ltac/tacarg.ml +++ b/plugins/ltac/tacarg.ml @@ -19,13 +19,19 @@ let make0 ?dyn name = let () = Geninterp.register_val0 wit dyn in wit -let wit_intro_pattern = make0 "intropattern" +let wit_intropattern = make0 "intropattern" (* To keep after deprecation phase but it will get a different parsing semantics (Tactic Notation and TACTIC EXTEND) in pltac.ml *) +let wit_simple_intropattern = make0 "simple_intropattern" let wit_quant_hyp = make0 "quant_hyp" let wit_constr_with_bindings = make0 "constr_with_bindings" let wit_open_constr_with_bindings = make0 "open_constr_with_bindings" let wit_bindings = make0 "bindings" let wit_quantified_hypothesis = wit_quant_hyp -let wit_intropattern = wit_intro_pattern + +(* A convenient common part to simple_intropattern and intropattern + usable when no parsing rule is concerned: indeed + simple_intropattern and intropattern are in the same type and have + the same interp/intern/subst methods *) +let wit_intro_pattern = wit_intropattern let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type = make0 "tactic" |