aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrparser.mlg48
-rw-r--r--plugins/ssr/ssrvernac.mlg8
2 files changed, 28 insertions, 28 deletions
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 7b584b5159..70dab585bf 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -100,7 +100,7 @@ ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma }
END
GRAMMAR EXTEND Gram
GLOBAL: ssrtacarg;
- ssrtacarg: [[ tac = tactic_expr LEVEL "5" -> { tac } ]];
+ ssrtacarg: [[ tac = ltac_expr LEVEL "5" -> { tac } ]];
END
(* Copy of ssrtacarg with LEVEL "3", useful for: "under ... do ..." *)
@@ -108,7 +108,7 @@ ARGUMENT EXTEND ssrtac3arg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma }
END
GRAMMAR EXTEND Gram
GLOBAL: ssrtac3arg;
- ssrtac3arg: [[ tac = tactic_expr LEVEL "3" -> { tac } ]];
+ ssrtac3arg: [[ tac = ltac_expr LEVEL "3" -> { tac } ]];
END
{
@@ -1337,7 +1337,7 @@ ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinde
GRAMMAR EXTEND Gram
GLOBAL: ssrbinder;
ssrbinder: [
- [ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> {
+ [ ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" -> {
(FwdPose, [BFvar]),
CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Glob_term.Explicit,c)],mkCHole (Some loc)) } ]
];
@@ -1594,18 +1594,18 @@ GRAMMAR EXTEND Gram
| n = Prim.natural -> { ArgArg (check_index ~loc n) }
] ];
ssrswap: [[ IDENT "first" -> { loc, true } | IDENT "last" -> { loc, false } ]];
- ssrorelse: [[ "||"; tac = tactic_expr LEVEL "2" -> { tac } ]];
+ ssrorelse: [[ "||"; tac = ltac_expr LEVEL "2" -> { tac } ]];
ssrseqarg: [
[ arg = ssrswap -> { noindex, swaptacarg arg }
| i = ssrseqidx; tac = ssrortacarg; def = OPT ssrorelse -> { i, (tac, def) }
| i = ssrseqidx; arg = ssrswap -> { i, swaptacarg arg }
- | tac = tactic_expr LEVEL "3" -> { noindex, (mk_hint tac, None) }
+ | tac = ltac_expr LEVEL "3" -> { noindex, (mk_hint tac, None) }
] ];
END
{
-let tactic_expr = Pltac.tactic_expr
+let ltac_expr = Pltac.ltac_expr
}
@@ -1688,9 +1688,9 @@ let tclintros_expr ?loc tac ipats =
}
GRAMMAR EXTEND Gram
- GLOBAL: tactic_expr;
- tactic_expr: LEVEL "1" [ RIGHTA
- [ tac = tactic_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros }
+ GLOBAL: ltac_expr;
+ ltac_expr: LEVEL "1" [ RIGHTA
+ [ tac = ltac_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros }
] ];
END
@@ -1704,9 +1704,9 @@ END
(* (Removing user-specified parentheses is dubious anyway). *)
GRAMMAR EXTEND Gram
- GLOBAL: tactic_expr;
- ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> { CAst.make ~loc (Tacexp tac) } ]];
- tactic_expr: LEVEL "0" [[ arg = ssrparentacarg -> { TacArg arg } ]];
+ GLOBAL: ltac_expr;
+ ssrparentacarg: [[ "("; tac = ltac_expr; ")" -> { CAst.make ~loc (Tacexp tac) } ]];
+ ltac_expr: LEVEL "0" [[ arg = ssrparentacarg -> { TacArg arg } ]];
END
(** The internal "done" and "ssrautoprop" tactics. *)
@@ -1741,7 +1741,7 @@ let tclBY tac = Tacticals.New.tclTHEN tac (donetac ~-1)
(* The latter two are used in forward-chaining tactics (have, suffice, wlog) *)
(* and subgoal reordering tacticals (; first & ; last), respectively. *)
-(* Force use of the tactic_expr parsing entry, to rule out tick marks. *)
+(* Force use of the ltac_expr parsing entry, to rule out tick marks. *)
(** The "by" tactical. *)
@@ -1782,12 +1782,12 @@ let ssrdotac_expr ?loc n m tac clauses =
}
GRAMMAR EXTEND Gram
- GLOBAL: tactic_expr;
+ GLOBAL: ltac_expr;
ssrdotac: [
- [ tac = tactic_expr LEVEL "3" -> { mk_hint tac }
+ [ tac = ltac_expr LEVEL "3" -> { mk_hint tac }
| tacs = ssrortacarg -> { tacs }
] ];
- tactic_expr: LEVEL "3" [ RIGHTA
+ ltac_expr: LEVEL "3" [ RIGHTA
[ IDENT "do"; m = ssrmmod; tac = ssrdotac; clauses = ssrclauses ->
{ ssrdotac_expr ~loc noindex m tac clauses }
| IDENT "do"; tac = ssrortacarg; clauses = ssrclauses ->
@@ -1833,20 +1833,20 @@ let tclseq_expr ?loc tac dir arg =
}
GRAMMAR EXTEND Gram
- GLOBAL: tactic_expr;
+ GLOBAL: ltac_expr;
ssr_first: [
[ tac = ssr_first; ipats = ssrintros_ne -> { tclintros_expr ~loc tac ipats }
- | "["; tacl = LIST0 tactic_expr SEP "|"; "]" -> { TacFirst tacl }
+ | "["; tacl = LIST0 ltac_expr SEP "|"; "]" -> { TacFirst tacl }
] ];
ssr_first_else: [
[ tac1 = ssr_first; tac2 = ssrorelse -> { TacOrelse (tac1, tac2) }
| tac = ssr_first -> { tac } ]];
- tactic_expr: LEVEL "4" [ LEFTA
- [ tac1 = tactic_expr; ";"; IDENT "first"; tac2 = ssr_first_else ->
+ ltac_expr: LEVEL "4" [ LEFTA
+ [ tac1 = ltac_expr; ";"; IDENT "first"; tac2 = ssr_first_else ->
{ TacThen (tac1, tac2) }
- | tac = tactic_expr; ";"; IDENT "first"; arg = ssrseqarg ->
+ | tac = ltac_expr; ";"; IDENT "first"; arg = ssrseqarg ->
{ tclseq_expr ~loc tac L2R arg }
- | tac = tactic_expr; ";"; IDENT "last"; arg = ssrseqarg ->
+ | tac = ltac_expr; ";"; IDENT "last"; arg = ssrseqarg ->
{ tclseq_expr ~loc tac R2L arg }
] ];
END
@@ -2447,8 +2447,8 @@ END
(* The standard TACTIC EXTEND does not work for abstract *)
GRAMMAR EXTEND Gram
- GLOBAL: tactic_expr;
- tactic_expr: LEVEL "3"
+ GLOBAL: ltac_expr;
+ ltac_expr: LEVEL "3"
[ RIGHTA [ IDENT "abstract"; gens = ssrdgens ->
{ ssrtac_expr ~loc "abstract"
[Tacexpr.TacGeneric (None, Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] } ]];
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 91cd5b251c..a49a5e8b28 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -85,7 +85,7 @@ let mk_pat c (na, t) = (c, na, t)
GRAMMAR EXTEND Gram
GLOBAL: binder_constr;
- ssr_rtype: [[ "return"; t = operconstr LEVEL "100" -> { mk_rtype t } ]];
+ ssr_rtype: [[ "return"; t = term LEVEL "100" -> { mk_rtype t } ]];
ssr_mpat: [[ p = pattern -> { [[p]] } ]];
ssr_dpat: [
[ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> { mp, mk_ctype mp t, rt }
@@ -96,9 +96,9 @@ GRAMMAR EXTEND Gram
ssr_elsepat: [[ "else" -> { [[CAst.make ~loc @@ CPatAtom None]] } ]];
ssr_else: [[ mp = ssr_elsepat; c = lconstr -> { CAst.make ~loc (mp, c) } ]];
binder_constr: [
- [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else ->
+ [ "if"; c = term LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else ->
{ let b1, ct, rt = db1 in CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) }
- | "if"; c = operconstr LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else ->
+ | "if"; c = term LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else ->
{ let b1, ct, rt = db1 in
let b1, b2 = let open CAst in
let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in
@@ -119,7 +119,7 @@ END
GRAMMAR EXTEND Gram
GLOBAL: closed_binder;
closed_binder: [
- [ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" ->
+ [ ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" ->
{ [CLocalAssum ([CAst.make ~loc Anonymous], Default Explicit, c)] }
] ];
END
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 18:41:15 +0000