Change a few nonterminal names in mlgs and update doc to match

7 files changed, 35 insertions, 35 deletions

diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index 122b0f5dfb..ba0ec28f8b 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -342,9 +342,9 @@ Recursive functions: fix
 .. insertprodn term_fix fixannot
 
 .. prodn::
-   term_fix ::= let fix @fix_body in @term
-   | fix @fix_body {? {+ with @fix_body } for @ident }
-   fix_body ::= @ident {* @binder } {? @fixannot } {? : @type } := @term
+   term_fix ::= let fix @fix_decl in @term
+   | fix @fix_decl {? {+ with @fix_decl } for @ident }
+   fix_decl ::= @ident {* @binder } {? @fixannot } {? : @type } := @term
    fixannot ::= %{ struct @ident %}
    | %{ wf @one_term @ident %}
    | %{ measure @one_term {? @ident } {? @one_term } %}
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 770de9a6c3..cdbae8ade1 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -5724,11 +5724,11 @@ respectively.
 
    local function definition
 
-.. tacv:: pose fix @fix_body
+.. tacv:: pose fix @fix_decl
 
    local fix definition
 
-.. tacv:: pose cofix @fix_body
+.. tacv:: pose cofix @fix_decl
 
    local cofix definition
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 754e73badf..f6a684bbd7 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -271,7 +271,7 @@ binder_constr: [
 | 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_body "in" term200
+| MOVETO term_fix "let" "fix" fix_decl "in" term200
 | MOVETO term_cofix "let" "cofix" cofix_body "in" term200
 | MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200
 | MOVETO term_let "let" "'" pattern200 ":=" term200 "in" term200
@@ -401,9 +401,9 @@ term0: [
 ]
 
 fix_decls: [
-| DELETE fix_body
-| REPLACE fix_body "with" LIST1 fix_body SEP "with" "for" identref
-| WITH fix_body OPT ( LIST1 ("with" fix_body) "for" identref )
+| DELETE fix_decl
+| REPLACE fix_decl "with" LIST1 fix_decl SEP "with" "for" identref
+| WITH fix_decl OPT ( LIST1 ("with" fix_decl) "for" identref )
 ]
 
 cofix_decls: [
@@ -1159,8 +1159,8 @@ command: [
 | "SubClass" ident_decl def_body
 | REPLACE "Ltac" LIST1 ltac_tacdef_body SEP "with"
 | WITH "Ltac" ltac_tacdef_body LIST0 ( "with" ltac_tacdef_body )
-| REPLACE "Function" LIST1 function_rec_definition_loc SEP "with"      (* funind plugin *)
-| WITH "Function" function_rec_definition_loc LIST0 ( "with" function_rec_definition_loc )      (* funind plugin *)
+| REPLACE "Function" LIST1 function_fix_definition SEP "with"      (* funind plugin *)
+| WITH "Function" function_fix_definition LIST0 ( "with" function_fix_definition )      (* funind plugin *)
 | REPLACE "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with"      (* funind plugin *)
 | WITH "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg )      (* funind plugin *)
 | DELETE "Cd"
@@ -2347,7 +2347,7 @@ SPLICE: [
 | check_module_types
 | constr_pattern
 | decl_sep
-| function_rec_definition_loc (* loses funind annotation *)
+| function_fix_definition (* loses funind annotation *)
 | glob
 | glob_constr_with_bindings
 | id_or_meta
@@ -2518,7 +2518,7 @@ SPLICE: [
 | ltac_defined_tactics
 | tactic_notation_tactics
 ]
-(* todo: ssrreflect*.rst ref to fix_body is incorrect *)
+(* todo: ssrreflect*.rst ref to fix_decl is incorrect *)
 
 REACHABLE: [
 | command
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 97d670522d..c764cb6f37 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -143,7 +143,7 @@ binder_constr: [
 | "forall" open_binders "," term200
 | "fun" open_binders "=>" term200
 | "let" name binders let_type_cstr ":=" term200 "in" term200
-| "let" "fix" fix_body "in" term200
+| "let" "fix" fix_decl "in" term200
 | "let" "cofix" cofix_body "in" term200
 | "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200
 | "let" "'" pattern200 ":=" term200 "in" term200
@@ -193,8 +193,8 @@ universe_level: [
 ]
 
 fix_decls: [
-| fix_body
-| fix_body "with" LIST1 fix_body SEP "with" "for" identref
+| fix_decl
+| fix_decl "with" LIST1 fix_decl SEP "with" "for" identref
 ]
 
 cofix_decls: [
@@ -202,7 +202,7 @@ cofix_decls: [
 | cofix_body "with" LIST1 cofix_body SEP "with" "for" identref
 ]
 
-fix_body: [
+fix_decl: [
 | identref binders_fixannot type_cstr ":=" term200
 ]
 
@@ -569,7 +569,7 @@ command: [
 | "Show" "Extraction"      (* extraction plugin *)
 | "Set" "Firstorder" "Solver" tactic
 | "Print" "Firstorder" "Solver"
-| "Function" LIST1 function_rec_definition_loc SEP "with"      (* funind plugin *)
+| "Function" LIST1 function_fix_definition SEP "with"      (* funind plugin *)
 | "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with"      (* funind plugin *)
 | "Functional" "Case" fun_scheme_arg      (* funind plugin *)
 | "Generate" "graph" "for" reference      (* funind plugin *)
@@ -1789,7 +1789,7 @@ auto_using': [
 |      (* funind plugin *)
 ]
 
-function_rec_definition_loc: [
+function_fix_definition: [
 | Vernac.fix_definition      (* funind plugin *)
 ]
 
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 0827ccd193..12a7bc684d 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -320,11 +320,11 @@ univ_constraint: [
 ]
 
 term_fix: [
-| "let" "fix" fix_body "in" term
-| "fix" fix_body OPT ( LIST1 ( "with" fix_body ) "for" ident )
+| "let" "fix" fix_decl "in" term
+| "fix" fix_decl OPT ( LIST1 ( "with" fix_decl ) "for" ident )
 ]
 
-fix_body: [
+fix_decl: [
 | ident LIST0 binder OPT fixannot OPT ( ":" type ) ":=" term
 ]
 
@@ -885,6 +885,7 @@ command: [
 | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* ring plugin *)
 | "Print" "Fields"      (* ring plugin *)
 | "Number" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier
+| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier
 | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident )
 | "Typeclasses" "Transparent" LIST1 qualid
 | "Typeclasses" "Opaque" LIST1 qualid
@@ -909,7 +910,6 @@ command: [
 | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family
 | "Declare" "Left" "Step" one_term
 | "Declare" "Right" "Step" one_term
-| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier
 | "String" "Notation" qualid qualid qualid ":" scope_name
 | "SubClass" ident_decl def_body
 | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ]
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index a4660bfe8b..349e14bba3 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -219,7 +219,7 @@ GRAMMAR EXTEND Gram
           | _, _ -> 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_body; "in"; c = term 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) }
@@ -285,8 +285,8 @@ GRAMMAR EXTEND Gram
       | id = global -> { UNamed (GType id) } ] ]
   ;
   fix_decls:
-    [ [ dcl = fix_body -> { let (id,_,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) }
-      | dcl = fix_body; "with"; dcls = LIST1 fix_body SEP "with"; "for"; id = identref ->
+    [ [ dcl = fix_decl -> { let (id,_,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) }
+      | dcl = fix_decl; "with"; dcls = LIST1 fix_decl SEP "with"; "for"; id = identref ->
         { (id,List.map (fun x -> x.CAst.v) (dcl::dcls)) } ] ]
   ;
   cofix_decls:
@@ -294,7 +294,7 @@ GRAMMAR EXTEND Gram
       | dcl = cofix_body; "with"; dcls = LIST1 cofix_body SEP "with"; "for"; id = identref ->
         { (id,List.map (fun x -> x.CAst.v) (dcl::dcls)) } ] ]
   ;
-  fix_body:
+  fix_decl:
     [ [ id = identref; bl = binders_fixannot; ty = type_cstr; ":=";
         c = term LEVEL "200" ->
         { CAst.make ~loc (id,snd bl,fst bl,ty,c) } ] ]
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 4b46e09e57..ca6ae150a7 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -147,18 +147,18 @@ END
 module Vernac = Pvernac.Vernac_
 module Tactic = Pltac
 
-let (wit_function_rec_definition_loc : Vernacexpr.fixpoint_expr Loc.located Genarg.uniform_genarg_type) =
-  Genarg.create_arg "function_rec_definition_loc"
+let (wit_function_fix_definition : Vernacexpr.fixpoint_expr Loc.located Genarg.uniform_genarg_type) =
+  Genarg.create_arg "function_fix_definition"
 
-let function_rec_definition_loc =
-  Pcoq.create_generic_entry2 "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc)
+let function_fix_definition =
+  Pcoq.create_generic_entry2 "function_fix_definition" (Genarg.rawwit wit_function_fix_definition)
 
 }
 
 GRAMMAR EXTEND Gram
-  GLOBAL: function_rec_definition_loc ;
+  GLOBAL: function_fix_definition ;
 
-  function_rec_definition_loc:
+  function_fix_definition:
     [ [ g = Vernac.fix_definition -> { Loc.tag ~loc g } ]]
     ;
 
@@ -168,7 +168,7 @@ END
 
 let () =
   let raw_printer env sigma _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in
-  Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer
+  Pptactic.declare_extra_vernac_genarg_pprule wit_function_fix_definition raw_printer
 
 let is_proof_termination_interactively_checked recsl =
   List.exists (function
@@ -196,7 +196,7 @@ let is_interactive recsl =
 }
 
 VERNAC COMMAND EXTEND Function STATE CUSTOM
-| ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
+| ["Function" ne_function_fix_definition_list_sep(recsl,"with")]
     => { classify_funind recsl }
     -> {
          if is_interactive recsl then