Rename operconstr -> term

4 files changed, 8 insertions, 8 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
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 7b584b5159..77360052f8 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -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)) } ]
   ];
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