Review changes #1

doc/sphinx/addendum/implicit-coercions.rst

@@ -240,8 +240,8 @@ declaration, this constructor is declared as a coercion.
 
       Same as :cmd:`Identity Coercion` but locally to the current section.
 
-   .. cmdv:: SubClass @ident := @type
-      :name: SubClassVar
+   .. cmd:: "SubClass" @ident_decl @def_body
+      :name: SubClass
 
       If :n:`@type` is a class :n:`@ident'` applied to some arguments then
       :n:`@ident` is defined and an identity coercion of name
@@ -251,7 +251,7 @@ declaration, this constructor is declared as a coercion.
       :n:`Definition @ident := @type.`
       :n:`Identity Coercion Id_@ident_@ident' : @ident >-> @ident'`.
 
-   .. cmdv:: Local SubClass @ident := @type
+   .. cmdv:: Local SubClass @ident_decl @def_body
 
       Same as before but locally to the current section.
 

doc/sphinx/language/gallina-extensions.rst

@@ -840,7 +840,6 @@ Sections create local contexts which can be shared across multiple definitions.
    .. cmdv:: Variables {+ ( {+ @ident } : @type) }
              Hypothesis {+ ( {+ @ident } : @type) }
              Hypotheses {+ ( {+ @ident } : @type) }
-      :name: VariablesVar; HypothesisVar; HypothesesVar
 
       These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`.
 

doc/sphinx/user-extensions/syntax-extensions.rst

@@ -357,7 +357,7 @@ Thanks to reserved notations, the inductive, co-inductive, record, recursive and
 corecursive definitions can benefit from customized notations. To do this, insert
 a ``where`` notation clause after the definition of the (co)inductive type or
 (co)recursive term (or after the definition of each of them in case of mutual
-definitions). The exact syntax is given by :token:`decl_notation` for inductive,
+definitions). The exact syntax is given by :n:`@decl_notation` for inductive,
 co-inductive, recursive and corecursive definitions and in :ref:`record-types`
 for records. Here are examples:
 
@@ -873,7 +873,6 @@ notations are given below. The optional :production:`scope` is described in
                  : Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`].
                  : CoFixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`].
                  : [Local] Declare Custom Entry `ident`.
-   decl_notation : [where `string` := `term` [: `scope`] and … and `string` := `term` [: `scope`]].
    modifiers     : `modifier`, … , `modifier`
    modifier      : at level `num`
                  : in custom `ident`

doc/tools/docgram/common.edit_mlg

@@ -374,10 +374,27 @@ evar_instance: [
 
 gallina: [
 | DELETE assumptions_token inline assum_list
+| REPLACE OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with"
+| WITH OPT cumulativity_token private_token finite_token inductive_definition LIST0 ( "with" inductive_definition )
+| REPLACE "Fixpoint" LIST1 rec_definition SEP "with"
+| WITH "Fixpoint" rec_definition LIST0 ( "with" rec_definition )
+| REPLACE "Let" "Fixpoint" LIST1 rec_definition SEP "with"
+| WITH "Let" "Fixpoint" rec_definition LIST0 ( "with" rec_definition )
+| REPLACE "CoFixpoint" LIST1 corec_definition SEP "with"
+| WITH "CoFixpoint" corec_definition LIST0 ( "with" corec_definition )
+| REPLACE "Let" "CoFixpoint" LIST1 corec_definition SEP "with"
+| WITH "Let" "CoFixpoint" corec_definition LIST0 ( "with" corec_definition )
+| REPLACE "Scheme" LIST1 scheme SEP "with"
+| WITH "Scheme" scheme LIST0 ( "with" scheme )
 ]
 
-assumption_token: [
-| assumptions_token
+decl_notation: [
+| REPLACE "where" LIST1 one_decl_notation SEP decl_sep
+| WITH "where" one_decl_notation LIST0 ( decl_sep one_decl_notation )
+]
+
+assumptions_token: [
+| DELETENT
 ]
 
 inline: [
@@ -615,6 +632,14 @@ printable: [
 command: [
 | REPLACE "Print" printable
 | WITH printable
+| "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 "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with"      (* funind plugin *)
+| WITH "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg )      (* funind plugin *)
+
 ]
 
 only_parsing: [
@@ -642,7 +667,7 @@ decl_notation: [
 
 binder_tactic: [
 | REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5
-| WITH "let" OPT "rec" LIST1 let_clause SEP "with" "in" tactic_expr5
+| WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" tactic_expr5
 ]
 
 tactic_then_gen: [
@@ -672,6 +697,23 @@ vernac_aux: [
 | tactic_mode "."
 ]
 
+def_token: [
+| DELETE "SubClass" (* document separately from Definition and Example *)
+]
+
+assumption_token: [
+| REPLACE "Axiom"
+| WITH [ "Axiom" | "Axioms" ]
+| REPLACE "Conjecture"
+| WITH [ "Conjecture" | "Conjectures" ]
+| REPLACE "Hypothesis"
+| WITH [ "Hypothesis" | "Hypotheses" ]
+| REPLACE "Parameter"
+| WITH [ "Parameter" | "Parameters" ]
+| REPLACE "Variable"
+| WITH [ "Variable" | "Variables" ]
+]
+
 SPLICE: [
 | noedit_mode
 | command_entry
@@ -787,7 +829,6 @@ SPLICE: [
 | evar_instance
 | fix_decls
 | cofix_decls
-| assumptions_token
 | assum_list
 | assum_coe
 | inline
@@ -804,6 +845,7 @@ SPLICE: [
 | quoted_attributes  (* todo: splice or not? *)
 | printable
 | only_parsing
+| def_token
 ] (* end SPLICE *)
 
 RENAME: [

doc/tools/docgram/doc_grammar.ml

@@ -1700,9 +1700,9 @@ let process_rst g file args seen tac_prods cmd_prods =
       let start_index = index_of start !g.order in
       let end_index = index_of end_ !g.order in
       if start_index = None then
-        error "%s line %d: '%s' is undefined\n" file !linenum start;
+        error "%s line %d: '%s' is undefined in insertprodn\n" file !linenum start;
       if end_index = None then
-        error "%s line %d: '%s' is undefined\n" file !linenum end_;
+        error "%s line %d: '%s' is undefined in insertprodn\n" file !linenum end_;
       if start_index <> None && end_index <> None then
         check_range_consistency g start end_;
       match start_index, end_index with

doc/tools/docgram/orderedGrammar

@@ -124,16 +124,11 @@ record_binder_body: [
 ]
 
 assumption_token: [
-| "Axiom"
-| "Conjecture"
-| "Hypothesis"
-| "Parameter"
-| "Variable"
-| "Axioms"
-| "Conjectures"
-| "Hypotheses"
-| "Parameters"
-| "Variables"
+| [ "Axiom" | "Axioms" ]
+| [ "Conjecture" | "Conjectures" ]
+| [ "Parameter" | "Parameters" ]
+| [ "Hypothesis" | "Hypotheses" ]
+| [ "Variable" | "Variables" ]
 ]
 
 assumpt: [
@@ -378,14 +373,14 @@ subprf: [
 gallina: [
 | thm_token ident_decl LIST0 binder ":" term LIST0 [ "with" ident_decl LIST0 binder ":" term ]
 | assumption_token OPT ( "Inline" OPT ( "(" num ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ]
-| def_token ident_decl def_body
+| [ "Definition" | "Example" ] ident_decl def_body
 | "Let" ident def_body
-| OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with"
-| "Fixpoint" LIST1 fix_definition SEP "with"
-| "Let" "Fixpoint" LIST1 fix_definition SEP "with"
-| "CoFixpoint" LIST1 cofix_definition SEP "with"
-| "Let" "CoFixpoint" LIST1 cofix_definition SEP "with"
-| "Scheme" LIST1 scheme SEP "with"
+| OPT cumulativity_token private_token finite_token inductive_definition LIST0 ( "with" inductive_definition )
+| "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
+| "Let" "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
+| "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition )
+| "Let" "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition )
+| "Scheme" scheme LIST0 ( "with" scheme )
 | "Combined" "Scheme" ident "from" LIST1 ident SEP ","
 | "Register" qualid "as" qualid
 | "Register" "Inline" qualid
@@ -400,7 +395,7 @@ fix_definition: [
 ]
 
 decl_notations: [
-| "where" LIST1 decl_notation SEP "and"
+| "where" decl_notation LIST0 ( "and" decl_notation )
 ]
 
 decl_notation: [
@@ -468,12 +463,6 @@ thm_token: [
 | "Property"
 ]
 
-def_token: [
-| "Definition"
-| "Example"
-| "SubClass"
-]
-
 def_body: [
 | LIST0 binder ":=" OPT reduce term
 | LIST0 binder ":" term ":=" OPT reduce term
@@ -996,12 +985,12 @@ command: [
 | "Print" "Rewrite" "HintDb" ident
 | "Print" "Ltac" qualid
 | "Locate" "Ltac" qualid
-| "Ltac" LIST1 tacdef_body SEP "with"
+| "Ltac" tacdef_body LIST0 ( "with" tacdef_body )
 | "Print" "Ltac" "Signatures"
 | "Set" "Firstorder" "Solver" ltac_expr
 | "Print" "Firstorder" "Solver"
-| "Function" LIST1 fix_definition SEP "with"      (* funind plugin *)
-| "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with"      (* funind plugin *)
+| "Function" fix_definition LIST0 ( "with" fix_definition )
+| "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg )
 | "Extraction" qualid      (* extraction plugin *)
 | "Recursive" "Extraction" LIST1 qualid      (* extraction plugin *)
 | "Extraction" string LIST1 qualid      (* extraction plugin *)
@@ -1041,6 +1030,7 @@ command: [
 | "Print" "Fields"      (* setoid_ring plugin *)
 | "Numeral" "Notation" qualid qualid qualid ":" ident OPT numnotoption
 | "String" "Notation" qualid qualid qualid ":" ident
+| "SubClass" ident_decl def_body
 ]
 
 orient: [
@@ -1952,7 +1942,7 @@ ltac_expr: [
 
 binder_tactic: [
 | "fun" LIST1 fun_var "=>" ltac_expr
-| "let" OPT "rec" LIST1 let_clause SEP "with" "in" ltac_expr
+| "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr
 | "info" ltac_expr
 ]