Rename operconstr -> term

16 files changed, 208 insertions, 207 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 0c51361b64..94a705a4c6 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -510,7 +510,7 @@ Displaying information about notations
 
    The output for `Print Grammar constr` includes :cmd:`Notation` definitions,
    which are dynamically added to the grammar at run time.
-   For example, in the definition for `operconstr`, the production on the second line shown
+   For example, in the definition for `term`, the production on the second line shown
    here is defined by a :cmd:`Reserved Notation` command in `Notations.v`::
 
      | "50" LEFTA
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index f9aba5b1e1..36b20c0920 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -28,7 +28,7 @@ strategy_level_or_var: [
 | strategy_level
 ]
 
-operconstr0: [
+term0: [
 | "ltac" ":" "(" tactic_expr5 ")"
 ]
 
@@ -36,7 +36,7 @@ EXTRAARGS_natural: [ | DELETENT ]
 EXTRAARGS_lconstr:  [ | DELETENT ]
 EXTRAARGS_strategy_level: [ | DELETENT ]
 G_LTAC_hint: [ | DELETENT ]
-G_LTAC_operconstr0: [ | DELETENT ]
+G_LTAC_term0: [ | DELETENT ]
 
 G_REWRITE_binders: [
 | DELETE Pcoq.Constr.binders
@@ -263,35 +263,35 @@ RENAME: [
 ]
 
 case_item: [
-| REPLACE operconstr100 OPT [ "as" name ] OPT [ "in" pattern200 ]
-| WITH operconstr100 OPT ("as" name) OPT [ "in" pattern200 ]
+| REPLACE term100 OPT [ "as" name ] OPT [ "in" pattern200 ]
+| WITH term100 OPT ("as" name) OPT [ "in" pattern200 ]
 ]
 
 binder_constr: [
-| MOVETO term_forall_or_fun "forall" open_binders "," operconstr200
-| MOVETO term_forall_or_fun "fun" open_binders "=>" operconstr200
-| MOVETO term_let "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
-| MOVETO term_if "if" operconstr200 as_return_type "then" operconstr200 "else" operconstr200
-| MOVETO term_fix "let" "fix" fix_decl "in" operconstr200
-| MOVETO term_cofix "let" "cofix" cofix_decl "in" operconstr200
-| MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" operconstr200 "in" operconstr200
-| MOVETO term_let "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
-| MOVETO term_let "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
-| MOVETO term_let "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200
+| MOVETO term_forall_or_fun "forall" open_binders "," term200
+| MOVETO term_forall_or_fun "fun" open_binders "=>" term200
+| MOVETO term_let "let" name binders let_type_cstr ":=" term200 "in" term200
+| MOVETO term_if "if" term200 as_return_type "then" term200 "else" term200
+| MOVETO term_fix "let" "fix" fix_decl "in" term200
+| MOVETO term_cofix "let" "cofix" cofix_decl "in" term200
+| MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200
+| MOVETO term_let "let" "'" pattern200 ":=" term200 "in" term200
+| MOVETO term_let "let" "'" pattern200 ":=" term200 case_type "in" term200
+| MOVETO term_let "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200
 | MOVETO term_fix "fix" fix_decls
 | MOVETO term_cofix "cofix" cofix_decls
 ]
 
 term_let: [
-| REPLACE "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
-| WITH "let" name let_type_cstr ":=" operconstr200 "in" operconstr200
-| "let" name LIST1 binder let_type_cstr ":=" operconstr200 "in" operconstr200
+| REPLACE "let" name binders let_type_cstr ":=" term200 "in" term200
+| WITH "let" name let_type_cstr ":=" term200 "in" term200
+| "let" name LIST1 binder let_type_cstr ":=" term200 "in" term200
 (* Don't need to document that "( )" is equivalent to "()" *)
-| REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" operconstr200 "in" operconstr200
-| WITH "let" "(" LIST0 name SEP "," ")" as_return_type ":=" operconstr200 "in" operconstr200
-| REPLACE "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
-| WITH  "let" "'" pattern200 ":=" operconstr200 OPT case_type "in" operconstr200
-| DELETE "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
+| REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200
+| WITH "let" "(" LIST0 name SEP "," ")" as_return_type ":=" term200 "in" term200
+| REPLACE "let" "'" pattern200 ":=" term200 "in" term200
+| WITH  "let" "'" pattern200 ":=" term200 OPT case_type "in" term200
+| DELETE "let" "'" pattern200 ":=" term200 case_type "in" term200
 ]
 
 atomic_constr: [
@@ -337,20 +337,20 @@ scope_delimiter: [
 ]
 
 type: [
-| operconstr200
+| term200
 ]
 
-operconstr100: [
-| REPLACE operconstr99 "<:" operconstr200
-| WITH operconstr99 "<:" type
-| MOVETO term_cast operconstr99 "<:" type
-| REPLACE operconstr99 "<<:" operconstr200
-| WITH operconstr99 "<<:" type
-| MOVETO term_cast operconstr99 "<<:" type
-| REPLACE operconstr99 ":" operconstr200
-| WITH operconstr99 ":" type
-| MOVETO term_cast operconstr99 ":" type
-| MOVETO term_cast operconstr99 ":>"
+term100: [
+| REPLACE term99 "<:" term200
+| WITH term99 "<:" type
+| MOVETO term_cast term99 "<:" type
+| REPLACE term99 "<<:" term200
+| WITH term99 "<<:" type
+| MOVETO term_cast term99 "<<:" type
+| REPLACE term99 ":" term200
+| WITH term99 ":" type
+| MOVETO term_cast term99 ":" type
+| MOVETO term_cast term99 ":>"
 ]
 
 constr: [
@@ -359,43 +359,43 @@ constr: [
 | MOVETO term_explicit "@" qualid_annotated
 ]
 
-operconstr10: [
+term10: [
 (* Separate this LIST0 in the nonempty and the empty case *)
 (* The empty case is covered by constr *)
-| REPLACE "@" global univ_instance LIST0 operconstr9
-| WITH "@" qualid_annotated LIST1 operconstr9
-| REPLACE operconstr9
+| REPLACE "@" global univ_instance LIST0 term9
+| WITH "@" qualid_annotated LIST1 term9
+| REPLACE term9
 | WITH constr
-| MOVETO term_application operconstr9 LIST1 appl_arg
-| MOVETO term_application "@" qualid_annotated LIST1 operconstr9
+| MOVETO term_application term9 LIST1 appl_arg
+| MOVETO term_application "@" qualid_annotated LIST1 term9
 (* fixme: add in as a prodn somewhere *)
 | MOVETO dangling_pattern_extension_rule "@" pattern_ident LIST1 identref
 | DELETE dangling_pattern_extension_rule
 ]
 
-operconstr9: [
+term9: [
 (* @Zimmi48: Special token .. is for use in the Notation command. (see bug_3304.v) *)
-| DELETE ".." operconstr0 ".."
+| DELETE ".." term0 ".."
 ]
 
-operconstr1: [
-| REPLACE operconstr0 ".(" global LIST0 appl_arg ")"
-| WITH    operconstr0 ".(" global LIST0 appl_arg ")" (* huh? *)
-| REPLACE operconstr0 "%" IDENT
-| WITH operconstr0 "%" scope_key
-| MOVETO term_scope operconstr0 "%" scope_key
-| MOVETO term_projection operconstr0 ".(" global LIST0 appl_arg ")"
-| MOVETO term_projection operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")"
+term1: [
+| REPLACE term0 ".(" global LIST0 appl_arg ")"
+| WITH    term0 ".(" global LIST0 appl_arg ")" (* huh? *)
+| REPLACE term0 "%" IDENT
+| WITH term0 "%" scope_key
+| MOVETO term_scope term0 "%" scope_key
+| MOVETO term_projection term0 ".(" global LIST0 appl_arg ")"
+| MOVETO term_projection term0 ".(" "@" global LIST0 ( term9 ) ")"
 ]
 
-operconstr0: [
+term0: [
 (* @Zimmi48: This rule is a hack, according to Hugo, and should not be shown in the manual. *)
 | DELETE "{" binder_constr "}"
 | REPLACE "{|" record_declaration bar_cbrace
 | WITH "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace
 | MOVETO term_record "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace
-| MOVETO term_generalizing "`{" operconstr200 "}"
-| MOVETO term_generalizing "`(" operconstr200 ")"
+| MOVETO term_generalizing "`{" term200 "}"
+| MOVETO term_generalizing "`(" term200 ")"
 | MOVETO term_ltac "ltac" ":" "(" tactic_expr5 ")"
 | REPLACE "[" "|" array_elems "|" lconstr type_cstr "|" "]" univ_instance
 | WITH "[|" array_elems "|" lconstr type_cstr "|]" univ_instance
@@ -481,11 +481,11 @@ name_colon: [
 ]
 
 typeclass_constraint: [
-| EDIT ADD_OPT "!" operconstr200
-| REPLACE "{" name "}" ":" [ "!" | ] operconstr200
-| WITH "{" name "}" ":" OPT "!"  operconstr200
-| REPLACE name ":" [ "!" | ] operconstr200
-| WITH name ":" OPT "!" operconstr200
+| EDIT ADD_OPT "!" term200
+| REPLACE "{" name "}" ":" [ "!" | ] term200
+| WITH "{" name "}" ":" OPT "!"  term200
+| REPLACE name ":" [ "!" | ] term200
+| WITH name ":" OPT "!" term200
 ]
 
 (* ?? From the grammar, Prim.name seems to be only "_" but ident is also accepted "*)
@@ -731,7 +731,7 @@ gallina_ext: [
 | WITH "Set" option_table option_setting
 | REPLACE "Export" "Unset" option_table
 | WITH "Unset" option_table
-| REPLACE "Instance" instance_name ":" operconstr200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ]
+| REPLACE "Instance" instance_name ":" term200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ]
 | WITH "Instance" instance_name ":" type hint_info OPT [ ":=" "{" record_declaration "}" | ":=" lconstr ]
 
 | REPLACE "From" global "Require" export_token LIST1 global
@@ -1944,7 +1944,7 @@ tactic_notation_tactics: [
 
 (* defined in OCaml outside of mlgs *)
 tactic_arg: [
-| "uconstr" ":" "(" operconstr200 ")"
+| "uconstr" ":" "(" term200 ")"
 | MOVEALLBUT simple_tactic
 ]
 
@@ -2309,10 +2309,10 @@ SPLICE: [
 | ltac_selector
 | Constr.ident
 | attribute_list
-| operconstr99
-| operconstr90
-| operconstr9
-| operconstr8
+| term99
+| term90
+| term9
+| term8
 | pattern200
 | pattern99
 | pattern90
@@ -2499,11 +2499,7 @@ RENAME: [
 
 (* | nonsimple_intropattern intropattern (* ltac2 *) *)
 
-| operconstr200 term   (* historical name *)
-| operconstr100 term100
-| operconstr10 term10
-| operconstr1 term1
-| operconstr0 term0
+| term200 term
 | pattern100 pattern
 | match_constr term_match
 (*| impl_ident_tail impl_ident*)
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index d3148b5e3a..9a2e4cd8e7 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -58,67 +58,67 @@ universe: [
 ]
 
 lconstr: [
-| operconstr200
+| term200
 ]
 
 constr: [
-| operconstr8
+| term8
 | "@" global univ_instance
 ]
 
-operconstr200: [
+term200: [
 | binder_constr
-| operconstr100
+| term100
 ]
 
-operconstr100: [
-| operconstr99 "<:" operconstr200
-| operconstr99 "<<:" operconstr200
-| operconstr99 ":" operconstr200
-| operconstr99 ":>"
-| operconstr99
+term100: [
+| term99 "<:" term200
+| term99 "<<:" term200
+| term99 ":" term200
+| term99 ":>"
+| term99
 ]
 
-operconstr99: [
-| operconstr90
+term99: [
+| term90
 ]
 
-operconstr90: [
-| operconstr10
+term90: [
+| term10
 ]
 
-operconstr10: [
-| operconstr9 LIST1 appl_arg
-| "@" global univ_instance LIST0 operconstr9
-| "@" pattern_ident LIST1 identref
-| operconstr9
+term10: [
+| term9 LIST1 appl_arg
+| "@" global univ_instance LIST0 term9
+| "@" pattern_identref LIST1 identref
+| term9
 ]
 
-operconstr9: [
-| ".." operconstr0 ".."
-| operconstr8
+term9: [
+| ".." term0 ".."
+| term8
 ]
 
-operconstr8: [
-| operconstr1
+term8: [
+| term1
 ]
 
-operconstr1: [
-| operconstr0 ".(" global LIST0 appl_arg ")"
-| operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")"
-| operconstr0 "%" IDENT
-| operconstr0
+term1: [
+| term0 ".(" global LIST0 appl_arg ")"
+| term0 ".(" "@" global LIST0 ( term9 ) ")"
+| term0 "%" IDENT
+| term0
 ]
 
-operconstr0: [
+term0: [
 | atomic_constr
 | match_constr
-| "(" operconstr200 ")"
+| "(" term200 ")"
 | "{|" record_declaration bar_cbrace
 | "{" binder_constr "}"
-| "`{" operconstr200 "}"
+| "`{" term200 "}"
 | test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_instance
-| "`(" operconstr200 ")"
+| "`(" term200 ")"
 ]
 
 array_elems: [
@@ -140,23 +140,23 @@ field_def: [
 ]
 
 binder_constr: [
-| "forall" open_binders "," operconstr200
-| "fun" open_binders "=>" operconstr200
-| "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
-| "let" "fix" fix_decl "in" operconstr200
-| "let" "cofix" cofix_decl "in" operconstr200
-| "let" [ "(" LIST0 name SEP "," ")" | "()" ] return_type ":=" operconstr200 "in" operconstr200
-| "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
-| "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
-| "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200
-| "if" operconstr200 return_type "then" operconstr200 "else" operconstr200
+| "forall" open_binders "," term200
+| "fun" open_binders "=>" term200
+| "let" name binders let_type_cstr ":=" term200 "in" term200
+| "let" "fix" fix_decl "in" term200
+| "let" "cofix" cofix_decl "in" term200
+| "let" [ "(" LIST0 name SEP "," ")" | "()" ] return_type ":=" term200 "in" term200
+| "let" "'" pattern200 ":=" term200 "in" term200
+| "let" "'" pattern200 ":=" term200 case_type "in" term200
+| "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200
+| "if" term200 return_type "then" term200 "else" term200
 | "fix" fix_decls
 | "cofix" cofix_decls
 ]
 
 appl_arg: [
-| test_lpar_id_coloneq "(" identref ":=" lconstr ")"
-| operconstr9
+| test_lpar_id_coloneq "(" ident ":=" lconstr ")"
+| term9
 ]
 
 atomic_constr: [
@@ -165,13 +165,13 @@ atomic_constr: [
 | NUMBER
 | string
 | "_"
-| "?" "[" identref "]"
+| "?" "[" ident "]"
 | "?" "[" pattern_ident "]"
 | pattern_ident evar_instance
 ]
 
 inst: [
-| identref ":=" lconstr
+| ident ":=" lconstr
 ]
 
 evar_instance: [
@@ -203,11 +203,11 @@ cofix_decls: [
 ]
 
 fix_decl: [
-| identref binders_fixannot type_cstr ":=" operconstr200
+| identref binders_fixannot type_cstr ":=" term200
 ]
 
 cofix_decl: [
-| identref binders type_cstr ":=" operconstr200
+| identref binders type_cstr ":=" term200
 ]
 
 match_constr: [
@@ -215,11 +215,11 @@ match_constr: [
 ]
 
 case_item: [
-| operconstr100 OPT [ "as" name ] OPT [ "in" pattern200 ]
+| term100 OPT [ "as" name ] OPT [ "in" pattern200 ]
 ]
 
 case_type: [
-| "return" operconstr100
+| "return" term100
 ]
 
 return_type: [
@@ -253,7 +253,7 @@ pattern200: [
 ]
 
 pattern100: [
-| pattern99 ":" operconstr200
+| pattern99 ":" term200
 | pattern99
 ]
 
@@ -335,10 +335,10 @@ closed_binder: [
 ]
 
 typeclass_constraint: [
-| "!" operconstr200
-| "{" name "}" ":" [ "!" | ] operconstr200
-| test_name_colon name ":" [ "!" | ] operconstr200
-| operconstr200
+| "!" term200
+| "{" name "}" ":" [ "!" | ] term200
+| test_name_colon name ":" [ "!" | ] term200
+| term200
 ]
 
 type_cstr: [
@@ -362,12 +362,16 @@ pattern_ident: [
 | LEFTQMARK ident
 ]
 
-identref: [
+pattern_identref: [
+| pattern_ident
+]
+
+var: [
 | ident
 ]
 
-hyp: [
-| identref
+identref: [
+| ident
 ]
 
 field: [
@@ -506,7 +510,7 @@ command: [
 | "Remove" "Hints" LIST1 global opt_hintbases
 | "Hint" hint opt_hintbases
 | "Comments" LIST0 comment
-| "Declare" "Instance" ident_decl binders ":" operconstr200 hint_info
+| "Declare" "Instance" ident_decl binders ":" term200 hint_info
 | "Declare" "Scope" IDENT
 | "Pwd"
 | "Cd"
@@ -592,9 +596,9 @@ command: [
 | "Optimize" "Proof"
 | "Optimize" "Heap"
 | "Hint" "Cut" "[" hints_path "]" opthints
-| "Typeclasses" "Transparent" LIST1 reference
-| "Typeclasses" "Opaque" LIST1 reference
-| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT natural
+| "Typeclasses" "Transparent" LIST0 reference
+| "Typeclasses" "Opaque" LIST0 reference
+| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT integer
 | "Proof" "with" Pltac.tactic OPT [ "using" G_vernac.section_subset_expr ]
 | "Proof" "using" G_vernac.section_subset_expr OPT [ "with" Pltac.tactic ]
 | "Tactic" "Notation" OPT ltac_tactic_level LIST1 ltac_production_item ":=" tactic
@@ -611,7 +615,6 @@ command: [
 | "Solve" "Obligation" natural "of" ident "with" tactic
 | "Solve" "Obligation" natural "with" tactic
 | "Solve" "Obligations" "of" ident "with" tactic
-| "Solve" "Obligations" "of" ident
 | "Solve" "Obligations" "with" tactic
 | "Solve" "Obligations"
 | "Solve" "All" "Obligations" "with" tactic
@@ -1011,7 +1014,7 @@ gallina_ext: [
 | "Coercion" global ":" class_rawexpr ">->" class_rawexpr
 | "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr
 | "Context" LIST1 binder
-| "Instance" instance_name ":" operconstr200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ]
+| "Instance" instance_name ":" term200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ]
 | "Existing" "Instance" global hint_info
 | "Existing" "Instances" LIST1 global OPT [ "|" natural ]
 | "Existing" "Class" global
@@ -1548,7 +1551,7 @@ simple_tactic: [
 | "notypeclasses" "refine" uconstr
 | "simple" "notypeclasses" "refine" uconstr
 | "solve_constraints"
-| "subst" LIST1 hyp
+| "subst" LIST1 var
 | "subst"
 | "simple" "subst"
 | "evar" test_lpar_id_colon "(" ident ":" lconstr ")"
@@ -1616,7 +1619,6 @@ simple_tactic: [
 | "convert_concl_no_check" constr
 | "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident
 | "typeclasses" "eauto" OPT int_or_var "with" LIST1 preident
-| "typeclasses" "eauto" "bfs" OPT int_or_var
 | "typeclasses" "eauto" OPT int_or_var
 | "head_of_constr" ident constr
 | "not_evar" constr
@@ -1809,7 +1811,7 @@ EXTRAARGS_natural: [
 
 occurrences: [
 | LIST1 integer
-| hyp
+| var
 ]
 
 glob: [
@@ -2147,7 +2149,7 @@ G_LTAC_hint: [
 | "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic
 ]
 
-G_LTAC_operconstr0: [
+G_LTAC_term0: [
 | "ltac" ":" "(" Pltac.tactic_expr ")"
 ]
 
@@ -2327,7 +2329,7 @@ intropattern: [
 ]
 
 simple_intropattern: [
-| simple_intropattern_closed LIST0 [ "%" operconstr0 ]
+| simple_intropattern_closed LIST0 [ "%" term0 ]
 ]
 
 simple_intropattern_closed: [
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
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
diff --git a/test-suite/misc/quotation_token/src/quotation.mlg b/test-suite/misc/quotation_token/src/quotation.mlg
index 961b170a0d..ba0bcb1b3c 100644
--- a/test-suite/misc/quotation_token/src/quotation.mlg
+++ b/test-suite/misc/quotation_token/src/quotation.mlg
@@ -2,9 +2,9 @@
 open Pcoq.Constr
 }
 GRAMMAR EXTEND Gram
-  GLOBAL: operconstr;
+  GLOBAL: term;
 
-  operconstr: LEVEL "0"
+  term: LEVEL "0"
     [ [ s = QUOTATION "foobar:" ->
         {
           CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [GProp,0])) } ] ]
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index a42518822f..fa0c20bf73 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -8,7 +8,7 @@ Entry custom:myconstr is
 | "4" RIGHTA
   [ SELF; "*"; NEXT ]
 | "3" RIGHTA
-  [ "<"; operconstr LEVEL "10"; ">" ] ]
+  [ "<"; term LEVEL "10"; ">" ] ]
 
 [< b > + < b > * < 2 >]
      : nat
@@ -77,7 +77,7 @@ The command has indeed failed with message:
 The format is not the same on the right- and left-hand sides of the special token "..".
 Entry custom:expr is
 [ "201" RIGHTA
-  [ "{"; operconstr LEVEL "200"; "}" ] ]
+  [ "{"; term LEVEL "200"; "}" ] ]
 
 fun x : nat => [ x ]
      : nat -> nat
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index cecc6c66d2..2da5344496 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -497,7 +497,7 @@ GRAMMAR EXTEND Gram
   ;
   simple_intropattern:
     [ [ pat = simple_intropattern_closed ->
-(*         l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] -> *)
+(*         l = LIST0 ["%"; c = term LEVEL "0" -> c] -> *)
         (** TODO: handle %pat *)
         { pat }
     ] ]
@@ -812,7 +812,7 @@ END
 
 (*
 GRAMMAR EXTEND Gram
-  Pcoq.Constr.operconstr: LEVEL "0"
+  Pcoq.Constr.term: LEVEL "0"
     [ [ IDENT "ltac2"; ":"; "("; tac = tac2expr; ")" ->
       { let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in
         CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg)) }
@@ -867,7 +867,7 @@ let rules = [
 ] in
 
 Hook.set Tac2entries.register_constr_quotations begin fun () ->
-  Pcoq.grammar_extend Pcoq.Constr.operconstr {pos=Some (Gramlib.Gramext.Level "0"); data=[(None, None, rules)]}
+  Pcoq.grammar_extend Pcoq.Constr.term {pos=Some (Gramlib.Gramext.Level "0"); data=[(None, None, rules)]}
 end
 
 }
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index b134f7b82b..123ea2c24e 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -300,13 +300,13 @@ let interp_constr_entry_key : type r. _ -> r target -> int -> r Entry.t * int op
   match forpat with
   | ForConstr ->
     if level = 200 then Constr.binder_constr, None
-    else Constr.operconstr, Some level
+    else Constr.term, Some level
   | ForPattern -> Constr.pattern, Some level
 
 let target_entry : type s. notation_entry -> s target -> s Entry.t = function
 | InConstrEntry ->
    (function
-   | ForConstr -> Constr.operconstr
+   | ForConstr -> Constr.term
    | ForPattern -> Constr.pattern)
 | InCustomEntry s ->
    let (entry_for_constr, entry_for_patttern) = find_custom_entry s in
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index dfc7b05b51..4c08cf7f79 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -687,7 +687,7 @@ GRAMMAR EXTEND Gram
           { VernacContext (List.flatten c) }
 
       | IDENT "Instance"; namesup = instance_name; ":";
-         t = operconstr LEVEL "200";
+         t = term LEVEL "200";
          info = hint_info ;
          props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } |
              ":="; c = lconstr -> { Some (false,c) } | -> { None } ] ->
@@ -837,7 +837,7 @@ GRAMMAR EXTEND Gram
 
       (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *)
       | IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":";
-         t = operconstr LEVEL "200";
+         t = term LEVEL "200";
          info = hint_info ->
            { VernacDeclareInstance (id, bl, t, info) }
 
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 8ce59c40c3..185abcf35b 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -61,15 +61,15 @@ let pr_registered_grammar name =
     prlist pr_one entries
 
 let pr_grammar = function
-  | "constr" | "operconstr" | "binder_constr" ->
+  | "constr" | "term" | "binder_constr" ->
       str "Entry constr is" ++ fnl () ++
       pr_entry Pcoq.Constr.constr ++
       str "and lconstr is" ++ fnl () ++
       pr_entry Pcoq.Constr.lconstr ++
       str "where binder_constr is" ++ fnl () ++
       pr_entry Pcoq.Constr.binder_constr ++
-      str "and operconstr is" ++ fnl () ++
-      pr_entry Pcoq.Constr.operconstr
+      str "and term is" ++ fnl () ++
+      pr_entry Pcoq.Constr.term
   | "pattern" ->
       pr_entry Pcoq.Constr.pattern
   | "vernac" ->