diff options
| author | Jim Fehrle | 2020-10-11 18:39:16 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-10-27 12:15:35 -0700 |
| commit | b402adc12c00ba72046423d3a1737ccad517f70e (patch) | |
| tree | 1940efc064bf87b9b996a0e21eaa75e9b57605d4 /plugins/ltac | |
| parent | 5f5cddae48c08872107f30938dcc2f3c8d91f33a (diff) | |
Rename operconstr -> term
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/g_ltac.mlg | 4 | ||||
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 2d74323689..f8fbf0c2d0 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -76,7 +76,7 @@ let hint = G_proofs.hint GRAMMAR EXTEND Gram GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint tactic_mode constr_may_eval constr_eval toplevel_selector - operconstr; + term; tactic_then_last: [ [ "|"; lta = LIST0 (OPT tactic_expr) SEP "|" -> @@ -343,7 +343,7 @@ GRAMMAR EXTEND Gram tac = Pltac.tactic -> { Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ] ; - operconstr: LEVEL "0" + term: LEVEL "0" [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> { let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in CAst.make ~loc @@ CHole (None, IntroAnonymous, Some arg) } ] ] diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index c186a83a5c..18fc9ce9d4 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -291,7 +291,7 @@ GRAMMAR EXTEND Gram ; simple_intropattern: [ [ pat = simple_intropattern_closed; - l = LIST0 ["%"; c = operconstr LEVEL "0" -> { c } ] -> + l = LIST0 ["%"; c = term LEVEL "0" -> { c } ] -> { let {CAst.loc=loc0;v=pat} = pat in let f c pat = let loc1 = Constrexpr_ops.constr_loc c in |