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

3 files changed, 18 insertions, 18 deletions

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 ]