Merge PR #10149: [refman] Misc fixes (indentation, whitespace, notation syntax)

Reviewed-by: Zimmi48

2 files changed, 19 insertions, 19 deletions

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index ccd25ec9f3..5e214f6f7f 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -85,7 +85,7 @@ To build an object of type :token:`ident`, one should provide the constructor
 
   .. productionlist::
     record_term : {| [`field_def` ; … ; `field_def`] |}
-    field_def : name [binders] := `record_term`
+    field_def : `ident` [`binders`] := `term`
 
 Alternatively, the following syntax allows creating objects by using named fields, as
 shown in this grammar. The fields do not have to be in any particular order, nor do they have
@@ -831,16 +831,16 @@ Sections create local contexts which can be shared across multiple definitions.
 
       Links :token:`type` to each :token:`ident`.
 
-   .. cmdv:: Variable {+ ( {+ @ident } : @type ) }
+   .. cmdv:: Variable {+ ( {+ @ident } : @type ) }
 
       Declare one or more variables with various types.
 
-   .. cmdv:: Variables {+ ( {+ @ident } : @type) }
-             Hypothesis {+ ( {+ @ident } : @type) }
-             Hypotheses {+ ( {+ @ident } : @type) }
+   .. cmdv:: Variables {+ ( {+ @ident } : @type) }
+             Hypothesis {+ ( {+ @ident } : @type) }
+             Hypotheses {+ ( {+ @ident } : @type) }
       :name: Variables; Hypothesis; Hypotheses
 
-      These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`.
+      These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`.
 
 .. cmd:: Let @ident := @term
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 5a1af9f9fa..8acbcbec8f 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -616,34 +616,34 @@ has type :token:`type`.
 
       Adds several parameters with specification :token:`type`.
 
-   .. cmdv:: Parameter {+ ( {+ @ident } : @type ) }
+   .. cmdv:: Parameter {+ ( {+ @ident } : @type ) }
 
       Adds blocks of parameters with different specifications.
 
-   .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) }
+   .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) }
       :name: Local Parameter
 
       Such parameters are never made accessible through their unqualified name by
       :cmd:`Import` and its variants. You have to explicitly give their fully
       qualified name to refer to them.
 
-   .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) }
-             {? Local } Axiom {+ ( {+ @ident } : @type ) }
-             {? Local } Axioms {+ ( {+ @ident } : @type ) }
-             {? Local } Conjecture {+ ( {+ @ident } : @type ) }
-             {? Local } Conjectures {+ ( {+ @ident } : @type ) }
+   .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) }
+             {? Local } Axiom {+ ( {+ @ident } : @type ) }
+             {? Local } Axioms {+ ( {+ @ident } : @type ) }
+             {? Local } Conjecture {+ ( {+ @ident } : @type ) }
+             {? Local } Conjectures {+ ( {+ @ident } : @type ) }
       :name: Parameters; Axiom; Axioms; Conjecture; Conjectures
 
-      These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`.
+      These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`.
 
-   .. cmdv:: Variable  {+ ( {+ @ident } : @type ) }
-             Variables {+ ( {+ @ident } : @type ) }
-             Hypothesis {+ ( {+ @ident } : @type ) }
-             Hypotheses {+ ( {+ @ident } : @type ) }
+   .. cmdv:: Variable  {+ ( {+ @ident } : @type ) }
+             Variables {+ ( {+ @ident } : @type ) }
+             Hypothesis {+ ( {+ @ident } : @type ) }
+             Hypotheses {+ ( {+ @ident } : @type ) }
       :name: Variable (outside a section); Variables (outside a section); Hypothesis (outside a section); Hypotheses (outside a section)
 
       Outside of any section, these variants are synonyms of
-      :n:`Local Parameter {+ ( {+ @ident } : @type ) }`.
+      :n:`Local Parameter {+ ( {+ @ident } : @type ) }`.
       For their meaning inside a section, see :cmd:`Variable` in
       :ref:`section-mechanism`.