Rename operconstr -> term

3 files changed, 48 insertions, 45 deletions

diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 644493a010..bfd1fed6f0 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -80,7 +80,7 @@ let test_array_closing =
 }
 
 GRAMMAR EXTEND Gram
-  GLOBAL: binder_constr lconstr constr operconstr
+  GLOBAL: binder_constr lconstr constr term
   universe_level universe_name sort sort_family
   global constr_pattern lconstr_pattern Constr.ident
   closed_binder open_binders binder binders binders_fixannot
@@ -131,48 +131,48 @@ GRAMMAR EXTEND Gram
       | u = universe_expr -> { [u] } ] ]
   ;
   lconstr:
-    [ [ c = operconstr LEVEL "200" -> { c } ] ]
+    [ [ c = term LEVEL "200" -> { c } ] ]
   ;
   constr:
-    [ [ c = operconstr LEVEL "8" -> { c }
+    [ [ c = term LEVEL "8" -> { c }
       | "@"; f=global; i = univ_instance -> { CAst.make ~loc @@ CAppExpl((None,f,i),[]) } ] ]
   ;
-  operconstr:
+  term:
     [ "200" RIGHTA
       [ c = binder_constr -> { c } ]
     | "100" RIGHTA
-      [ c1 = operconstr; "<:"; c2 = operconstr LEVEL "200" ->
+      [ c1 = term; "<:"; c2 = term LEVEL "200" ->
                  { CAst.make ~loc @@ CCast(c1, CastVM c2) }
-      | c1 = operconstr; "<<:"; c2 = operconstr LEVEL "200" ->
+      | c1 = term; "<<:"; c2 = term LEVEL "200" ->
                  { CAst.make ~loc @@ CCast(c1, CastNative c2) }
-      | c1 = operconstr; ":"; c2 = operconstr LEVEL "200" ->
+      | c1 = term; ":"; c2 = term LEVEL "200" ->
                  { CAst.make ~loc @@ CCast(c1, CastConv c2) }
-      | c1 = operconstr; ":>" ->
+      | c1 = term; ":>" ->
                  { CAst.make ~loc @@ CCast(c1, CastCoerce) } ]
     | "99" RIGHTA [ ]
     | "90" RIGHTA [ ]
     | "10" LEFTA
-      [ f = operconstr; args = LIST1 appl_arg -> { CAst.make ~loc @@ CApp((None,f),args) }
+      [ f = term; args = LIST1 appl_arg -> { CAst.make ~loc @@ CApp((None,f),args) }
       | "@"; f = global; i = univ_instance; args = LIST0 NEXT -> { CAst.make ~loc @@ CAppExpl((None,f,i),args) }
       | "@"; lid = pattern_ident; args = LIST1 identref ->
         { let { CAst.loc = locid; v = id } = lid in
           let args = List.map (fun x -> CAst.make @@ CRef (qualid_of_ident ?loc:x.CAst.loc x.CAst.v, None), None) args in
           CAst.make ~loc @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) } ]
     | "9"
-      [ ".."; c = operconstr LEVEL "0"; ".." ->
+      [ ".."; c = term LEVEL "0"; ".." ->
         { CAst.make ~loc @@ CAppExpl ((None, (qualid_of_ident ~loc ldots_var), None),[c]) } ]
     | "8" [ ]
     | "1" LEFTA
-      [ c = operconstr; ".("; f = global; args = LIST0 appl_arg; ")" ->
+      [ c = term; ".("; f = global; args = LIST0 appl_arg; ")" ->
         { CAst.make ~loc @@ CApp((Some (List.length args+1), CAst.make @@ CRef (f,None)),args@[c,None]) }
-      | c = operconstr; ".("; "@"; f = global;
-        args = LIST0 (operconstr LEVEL "9"); ")" ->
+      | c = term; ".("; "@"; f = global;
+        args = LIST0 (term LEVEL "9"); ")" ->
         { CAst.make ~loc @@ CAppExpl((Some (List.length args+1),f,None),args@[c]) }
-      | c = operconstr; "%"; key = IDENT -> { CAst.make ~loc @@ CDelimiters (key,c) } ]
+      | c = term; "%"; key = IDENT -> { CAst.make ~loc @@ CDelimiters (key,c) } ]
     | "0"
       [ c = atomic_constr -> { c }
       | c = match_constr -> { c }
-      | "("; c = operconstr LEVEL "200"; ")" ->
+      | "("; c = term LEVEL "200"; ")" ->
         { (* Preserve parentheses around numerals so that constrintern does not
              collapse -(3) into the numeral -3. *)
           (match c.CAst.v with
@@ -182,14 +182,14 @@ GRAMMAR EXTEND Gram
       | "{|"; c = record_declaration; bar_cbrace -> { c }
       | "{"; c = binder_constr ; "}" ->
         { CAst.make ~loc @@ CNotation(None,(InConstrEntry,"{ _ }"),([c],[],[],[])) }
-      | "`{"; c = operconstr LEVEL "200"; "}" ->
+      | "`{"; c = term LEVEL "200"; "}" ->
         { CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) }
       | test_array_opening; "["; "|"; ls = array_elems; "|"; def = lconstr; ty = type_cstr; test_array_closing; "|"; "]"; u = univ_instance ->
         { let t = Array.make (List.length ls) def in
           List.iteri (fun i e -> t.(i) <- e) ls;
           CAst.make ~loc @@ CArray(u, t, def, ty)
         }
-      | "`("; c = operconstr LEVEL "200"; ")" ->
+      | "`("; c = term LEVEL "200"; ")" ->
         { CAst.make ~loc @@ CGeneralization (Explicit, None, c) } ] ]
   ;
   array_elems:
@@ -208,52 +208,52 @@ GRAMMAR EXTEND Gram
         { (id, mkLambdaCN ~loc bl c) } ] ]
   ;
   binder_constr:
-    [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" ->
+    [ [ "forall"; bl = open_binders; ","; c = term LEVEL "200" ->
         { mkProdCN ~loc bl c }
-      | "fun"; bl = open_binders; "=>"; c = operconstr LEVEL "200" ->
+      | "fun"; bl = open_binders; "=>"; c = term LEVEL "200" ->
         { mkLambdaCN ~loc bl c }
       | "let"; id=name; bl = binders; ty = let_type_cstr; ":=";
-        c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
+        c1 = term LEVEL "200"; "in"; c2 = term LEVEL "200" ->
         { let ty,c1 = match ty, c1 with
           | (_,None), { CAst.v = CCast(c, CastConv t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *)
           | _, _ -> ty, c1 in
           CAst.make ~loc @@ CLetIn(id,mkLambdaCN ?loc:(constr_loc c1) bl c1,
                  Option.map (mkProdCN ?loc:(fst ty) bl) (snd ty), c2) }
-      | "let"; "fix"; fx = fix_decl; "in"; c = operconstr LEVEL "200" ->
+      | "let"; "fix"; fx = fix_decl; "in"; c = term LEVEL "200" ->
         { let {CAst.loc=locf;CAst.v=({CAst.loc=li;CAst.v=id} as lid,_,_,_,_ as dcl)} = fx in
           let fix = CAst.make ?loc:locf @@ CFix (lid,[dcl]) in
           CAst.make ~loc @@ CLetIn( CAst.make ?loc:li @@ Name id,fix,None,c) }
-      | "let"; "cofix"; fx = cofix_decl; "in"; c = operconstr LEVEL "200" ->
+      | "let"; "cofix"; fx = cofix_decl; "in"; c = term LEVEL "200" ->
         { let {CAst.loc=locf;CAst.v=({CAst.loc=li;CAst.v=id} as lid,_,_,_ as dcl)} = fx in
           let cofix = CAst.make ?loc:locf @@ CCoFix (lid,[dcl]) in
           CAst.make ~loc @@ CLetIn( CAst.make ?loc:li @@ Name id,cofix,None,c) }
       | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> { l } | "()" -> { [] } ];
-        po = return_type; ":="; c1 = operconstr LEVEL "200"; "in";
-        c2 = operconstr LEVEL "200" ->
+        po = return_type; ":="; c1 = term LEVEL "200"; "in";
+        c2 = term LEVEL "200" ->
         { CAst.make ~loc @@ CLetTuple (lb,po,c1,c2) }
-      | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200";
-        "in"; c2 = operconstr LEVEL "200" ->
+      | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = term LEVEL "200";
+        "in"; c2 = term LEVEL "200" ->
         { CAst.make ~loc @@
           CCases (LetPatternStyle, None,    [c1, None, None],       [CAst.make ~loc ([[p]], c2)]) }
-      | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200";
-        rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
+      | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = term LEVEL "200";
+        rt = case_type; "in"; c2 = term LEVEL "200" ->
         { CAst.make ~loc @@
           CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [CAst.make ~loc ([[p]], c2)]) }
       | "let"; "'"; p = pattern LEVEL "200"; "in"; t = pattern LEVEL "200";
-        ":="; c1 = operconstr LEVEL "200"; rt = case_type;
-        "in"; c2 = operconstr LEVEL "200" ->
+        ":="; c1 = term LEVEL "200"; rt = case_type;
+        "in"; c2 = term LEVEL "200" ->
         { CAst.make ~loc @@
           CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [CAst.make ~loc ([[p]], c2)]) }
-      | "if"; c = operconstr LEVEL "200"; po = return_type;
-        "then"; b1 = operconstr LEVEL "200";
-        "else"; b2 = operconstr LEVEL "200" ->
+      | "if"; c = term LEVEL "200"; po = return_type;
+        "then"; b1 = term LEVEL "200";
+        "else"; b2 = term LEVEL "200" ->
         { CAst.make ~loc @@ CIf (c, po, b1, b2) }
       | "fix"; c = fix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CFix (id,dcls) }
       | "cofix"; c = cofix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CCoFix (id,dcls) } ] ]
   ;
   appl_arg:
     [ [ test_lpar_id_coloneq; "("; id = identref; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ?loc:id.CAst.loc @@ ExplByName id.CAst.v)) }
-      | c=operconstr LEVEL "9" -> { (c,None) } ] ]
+      | c=term LEVEL "9" -> { (c,None) } ] ]
   ;
   atomic_constr:
     [ [ g = global; i = univ_instance -> { CAst.make ~loc @@ CRef (g,i) }
@@ -294,14 +294,14 @@ GRAMMAR EXTEND Gram
       | dcl = cofix_decl; "with"; dcls = LIST1 cofix_decl SEP "with"; "for"; id = identref ->
         { (id,List.map (fun x -> x.CAst.v) (dcl::dcls)) } ] ]
   ;
-  fix_decl:
+  fix_decl:~loc @@ ExplByName id))
     [ [ id = identref; bl = binders_fixannot; ty = type_cstr; ":=";
-        c = operconstr LEVEL "200" ->
+        c = term LEVEL "200" ->
         { CAst.make ~loc (id,snd bl,fst bl,ty,c) } ] ]
   ;
   cofix_decl:
     [ [ id = identref; bl = binders; ty = type_cstr; ":=";
-        c = operconstr LEVEL "200" ->
+        c = term LEVEL "200" ->
         { CAst.make ~loc (id,bl,ty,c) } ] ]
   ;
   match_constr:
@@ -309,13 +309,13 @@ GRAMMAR EXTEND Gram
         br = branches; "end" -> { CAst.make ~loc @@ CCases(RegularStyle,ty,ci,br) } ] ]
   ;
   case_item:
-    [ [ c = operconstr LEVEL "100";
+    [ [ c = term LEVEL "100";
         ona = OPT ["as"; id = name -> { id } ];
         ty = OPT ["in"; t = pattern LEVEL "200" -> { t } ] ->
         { (c,ona,ty) } ] ]
   ;
   case_type:
-    [ [ "return"; ty = operconstr LEVEL "100" -> { ty } ] ]
+    [ [ "return"; ty = term LEVEL "100" -> { ty } ] ]
   ;
   return_type:
     [ [ a = OPT [ na = OPT["as"; na = name -> { na } ];
@@ -345,7 +345,7 @@ GRAMMAR EXTEND Gram
   pattern:
     [ "200" RIGHTA [ ]
     | "100" RIGHTA
-      [ p = pattern; ":"; ty = operconstr LEVEL "200" ->
+      [ p = pattern; ":"; ty = term LEVEL "200" ->
         { CAst.make ~loc @@ CPatCast (p, ty) } ]
     | "99" RIGHTA [ ]
     | "90" RIGHTA [ ]
@@ -447,12 +447,12 @@ GRAMMAR EXTEND Gram
           [CLocalPattern (CAst.make ~loc (p, ty))] } ] ]
   ;
   typeclass_constraint:
-    [ [ "!" ; c = operconstr LEVEL "200" -> { (CAst.make ~loc Anonymous), true, c }
-      | "{"; id = name; "}"; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = operconstr LEVEL "200" ->
+    [ [ "!" ; c = term LEVEL "200" -> { (CAst.make ~loc Anonymous), true, c }
+      | "{"; id = name; "}"; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = term LEVEL "200" ->
           { id, expl, c }
-      | test_name_colon; iid = name; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = operconstr LEVEL "200" ->
+      | test_name_colon; iid = name; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = term LEVEL "200" ->
           { iid, expl, c }
-      | c = operconstr LEVEL "200" ->
+      | c = term LEVEL "200" ->
           { (CAst.make ~loc Anonymous), false, c } ] ]
   ;
   type_cstr:
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 996aa0925c..ce73cee3be 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -308,7 +308,8 @@ module Constr =
 
     (* Entries that can be referred via the string -> Entry.t table *)
     let constr = Entry.create "constr"
-    let operconstr = Entry.create "operconstr"
+    let term = Entry.create "term"
+    let operconstr = term
     let constr_eoi = eoi_entry constr
     let lconstr = Entry.create "lconstr"
     let binder_constr = Entry.create "binder_constr"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 8e60bbf504..ccdf8abeda 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -185,7 +185,9 @@ module Constr :
     val constr_eoi : constr_expr Entry.t
     val lconstr : constr_expr Entry.t
     val binder_constr : constr_expr Entry.t
+    val term : constr_expr Entry.t
     val operconstr : constr_expr Entry.t
+      [@@deprecated "Deprecated in 8.13; use 'term' instead"]
     val ident : Id.t Entry.t
     val global : qualid Entry.t
     val universe_name : Glob_term.glob_sort_name Entry.t