From 211a241f81f80cfc17afc9f1f203a4a5805b8b4a Mon Sep 17 00:00:00 2001
From: Lysxia
Date: Sat, 16 Mar 2019 19:01:53 -0400
Subject: [Manual] Improve chapter Type classes, and add mention of Context
 under Variable

- More consistent code indentation
- Nest command variants properly
- Make `Context` explanation a bit less terse, with more links
- Typesetting bits, add some :cmd: links
---
 doc/sphinx/addendum/type-classes.rst               | 146 ++++++++++++---------
 .../language/gallina-specification-language.rst    |   3 +
 2 files changed, 84 insertions(+), 65 deletions(-)

diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index c7ea7e326f..a463a73bef 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -15,24 +15,25 @@ Class and Instance declarations
 The syntax for class and instance declarations is the same as the record
 syntax of Coq:
 
-``Class Id (`` |p_1| ``:`` |t_1| ``) ⋯ (`` |p_n| ``:`` |t_n| ``) [:
-sort] := {`` |f_1| ``:`` |u_1| ``; ⋮`` |f_m| ``:`` |u_m| ``}.``
+.. coqdoc::
 
-``Instance ident : Id`` |p_1| ``⋯`` |p_n| ``:= {`` |f_1| ``:=`` |t_1| ``; ⋮`` |f_m| ``:=`` |t_m| ``}.``
+  Class classname (p1 : t1) ⋯ (pn : tn) [: sort] := { f1 : u1 ; ⋯ ; fm : um }.
 
-The |p_i| ``:`` |t_i| variables are called the *parameters* of the class and
-the |f_i| ``:`` |t_i| are called the *methods*. Each class definition gives
+  Instance instancename q1 ⋯ qm : classname p1 ⋯ pn := { f1 := t1 ; ⋯ ; fm := tm }.
+
+The ``pi : ti`` variables are called the *parameters* of the class and
+the ``fi : ti`` are called the *methods*. Each class definition gives
 rise to a corresponding record declaration and each instance is a
-regular definition whose name is given by ident and type is an
+regular definition whose name is given by `instancename` and type is an
 instantiation of the record type.
 
 We’ll use the following example class in the rest of the chapter:
 
 .. coqtop:: in
 
-   Class EqDec (A : Type) := {
-     eqb : A -> A -> bool ;
-     eqb_leibniz : forall x y, eqb x y = true -> x = y }.
+   Class EqDec (A : Type) :=
+     { eqb : A -> A -> bool ;
+       eqb_leibniz : forall x y, eqb x y = true -> x = y }.
 
 This class implements a boolean equality test which is compatible with
 Leibniz equality on some type. An example implementation is:
@@ -40,9 +41,11 @@ Leibniz equality on some type. An example implementation is:
 .. coqtop:: in
 
    Instance unit_EqDec : EqDec unit :=
-    { eqb x y := true ;
-      eqb_leibniz x y H :=
-            match x, y return x = y with tt, tt => eq_refl tt end }.
+     { eqb x y := true ;
+       eqb_leibniz x y H :=
+         match x, y return x = y with
+         | tt, tt => eq_refl tt
+         end }.
 
 Using :cmd:`Program Instance`, if one does not give all the members in
 the Instance declaration, Coq generates obligations for the remaining
@@ -52,7 +55,7 @@ fields, e.g.:
 
    Require Import Program.Tactics.
    Program Instance eq_bool : EqDec bool :=
-   { eqb x y := if x then y else negb y }.
+     { eqb x y := if x then y else negb y }.
 
 .. coqtop:: all
 
@@ -127,9 +130,9 @@ the constraints as a binding context before the instance, e.g.:
 .. coqtop:: in
 
    Program Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) :=
-   { eqb x y := match x, y with
-                | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb)
-                end }.
+     { eqb x y := match x, y with
+                  | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb)
+                  end }.
 
 .. coqtop:: none
 
@@ -138,6 +141,8 @@ the constraints as a binding context before the instance, e.g.:
 These instances are used just as well as lemmas in the instance hint
 database.
 
+.. _contexts:
+
 Sections and contexts
 ---------------------
 
@@ -150,9 +155,9 @@ vernacular, except it accepts any binding context as argument. For example:
 
    Section EqDec_defs.
 
-     Context `{EA : EqDec A}.
+   Context `{EA : EqDec A}.
 
-     Global Program Instance option_eqb : EqDec (option A) :=
+   Global Program Instance option_eqb : EqDec (option A) :=
      { eqb x y := match x, y with
             | Some x, Some y => eqb x y
             | None, None => true
@@ -164,7 +169,7 @@ vernacular, except it accepts any binding context as argument. For example:
 
    About option_eqb.
 
-Here the Global modifier redeclares the instance at the end of the
+Here the :cmd:`Global` modifier redeclares the instance at the end of the
 section, once it has been generalized by the context variables it
 uses.
 
@@ -188,7 +193,7 @@ superclasses as a binding context:
 Contrary to Haskell, we have no special syntax for superclasses, but
 this declaration is equivalent to:
 
-::
+.. coqdoc::
 
     Class `(E : EqDec A) => Ord A :=
       { le : A -> A -> bool }.
@@ -248,8 +253,8 @@ explanation). These may be used as parts of other classes:
 .. coqtop:: all
 
    Class PreOrder (A : Type) (R : relation A) :=
-   { PreOrder_Reflexive :> Reflexive A R ;
-     PreOrder_Transitive :> Transitive A R }.
+     { PreOrder_Reflexive :> Reflexive A R ;
+       PreOrder_Transitive :> Transitive A R }.
 
 The syntax ``:>`` indicates that each ``PreOrder`` can be seen as a
 ``Reflexive`` relation. So each time a reflexive relation is needed, a
@@ -275,31 +280,29 @@ Summary of the commands
    The :cmd:`Class` command is used to declare a typeclass with parameters
    ``binders`` and fields the declared record fields.
 
-Variants:
+   .. _singleton-class:
 
-.. _singleton-class:
+   .. cmdv:: Class @ident {? @binders} : {? @sort} := @ident : @term
 
-.. cmd:: Class @ident {? @binders} : {? @sort} := @ident : @term
+      This variant declares a *singleton* class with a single method.  This
+      singleton class is a so-called definitional class, represented simply
+      as a definition ``ident binders := term`` and whose instances are
+      themselves objects of this type. Definitional classes are not wrapped
+      inside records, and the trivial projection of an instance of such a
+      class is convertible to the instance itself. This can be useful to
+      make instances of existing objects easily and to reduce proof size by
+      not inserting useless projections. The class constant itself is
+      declared rigid during resolution so that the class abstraction is
+      maintained.
 
-   This variant declares a *singleton* class with a single method.  This
-   singleton class is a so-called definitional class, represented simply
-   as a definition ``ident binders := term`` and whose instances are
-   themselves objects of this type. Definitional classes are not wrapped
-   inside records, and the trivial projection of an instance of such a
-   class is convertible to the instance itself. This can be useful to
-   make instances of existing objects easily and to reduce proof size by
-   not inserting useless projections. The class constant itself is
-   declared rigid during resolution so that the class abstraction is
-   maintained.
+   .. cmdv:: Existing Class @ident
 
-.. cmd:: Existing Class @ident
+      This variant declares a class a posteriori from a constant or
+      inductive definition. No methods or instances are defined.
 
-   This variant declares a class a posteriori from a constant or
-   inductive definition. No methods or instances are defined.
+      .. warn:: @ident is already declared as a typeclass
 
-   .. warn:: @ident is already declared as a typeclass
-
-      This command has no effect when used on a typeclass.
+         This command has no effect when used on a typeclass.
 
 .. cmd:: Instance @ident {? @binders} : @class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi }
 
@@ -314,32 +317,33 @@ Variants:
    :tacn:`auto` hints. If the priority is not specified, it defaults to the number
    of non-dependent binders of the instance.
 
-.. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @class @term__1 … @term__n [| priority] := @term
+   .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @class @term__1 … @term__n [| priority] := @term
 
-   This syntax is used for declaration of singleton class instances or
-   for directly giving an explicit term of type :n:`forall @binders, @class
-   @term__1 … @term__n`.  One need not even mention the unique field name for
-   singleton classes.
+      This syntax is used for declaration of singleton class instances or
+      for directly giving an explicit term of type :n:`forall @binders, @class
+      @term__1 … @term__n`.  One need not even mention the unique field name for
+      singleton classes.
 
-.. cmdv:: Global Instance
+   .. cmdv:: Global Instance
+      :name: Global Instance
 
-   One can use the ``Global`` modifier on instances declared in a
-   section so that their generalization is automatically redeclared
-   after the section is closed.
+      One can use the :cmd:`Global` modifier on instances declared in a
+      section so that their generalization is automatically redeclared
+      after the section is closed.
 
-.. cmdv:: Program Instance
-   :name: Program Instance
+   .. cmdv:: Program Instance
+      :name: Program Instance
 
-   Switches the type checking to Program (chapter :ref:`programs`) and
-   uses the obligation mechanism to manage missing fields.
+      Switches the type checking to `Program` (chapter :ref:`programs`) and
+      uses the obligation mechanism to manage missing fields.
 
-.. cmdv:: Declare Instance
-   :name: Declare Instance
+   .. cmdv:: Declare Instance
+      :name: Declare Instance
 
-   In a Module Type, this command states that a corresponding concrete
-   instance should exist in any implementation of this Module Type. This
-   is similar to the distinction between :cmd:`Parameter` vs. :cmd:`Definition`, or
-   between :cmd:`Declare Module` and :cmd:`Module`.
+      In a :cmd:`Module Type`, this command states that a corresponding concrete
+      instance should exist in any implementation of this :cmd:`Module Type`. This
+      is similar to the distinction between :cmd:`Parameter` vs. :cmd:`Definition`, or
+      between :cmd:`Declare Module` and :cmd:`Module`.
 
 
 Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a
@@ -356,8 +360,21 @@ few other commands related to typeclasses.
 
 .. cmd:: Context @binders
 
-   Declares variables according to the given binding context, which might
-   use :ref:`implicit-generalization`.
+   Declare variables in the context of the current section, like :cmd:`Variable`,
+   but also allowing implicit variables and :ref:`implicit-generalization`.
+
+   .. coqdoc::
+
+       Section ContextExample.
+
+       Context {A : Type} (a b : A).
+       Context `{EqDec A}.
+
+       (* ... *)
+
+       End ContextExample.
+
+   See also :ref:`contexts`.
 
 .. tacn:: typeclasses eauto
    :name: typeclasses eauto
@@ -449,9 +466,8 @@ By default, all constants and local variables are considered transparent. One
 should take care not to make opaque any constant that is used to abbreviate a
 type, like:
 
-::
-
-   relation A := A -> A -> Prop.
+.. coqdoc::
+   Definition relation A := A -> A -> Prop.
 
 This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``.
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 02fb9d84ce..158a3f5ffc 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -639,6 +639,9 @@ has type :token:`type`.
    parametrized (the variable is *discharged*). Using the :cmd:`Variable` command out
    of any section is equivalent to using :cmd:`Local Parameter`.
 
+   See also :cmd:`Context`, a variant of :cmd:`Variable` where variables can be
+   made implicit and allowing :ref:`implicit-generalization`.
+
    .. exn:: @ident already exists.
       :name: @ident already exists. (Variable)
       :undocumented:
-- 
cgit v1.2.3


From 911a3bf975ddb933acc0f7e17c465005a5ee8465 Mon Sep 17 00:00:00 2001
From: Lysxia
Date: Sat, 16 Mar 2019 20:49:02 -0400
Subject: [Manual] Gather section-specific commands in Section documentation
 (fix #9704)

---
 doc/sphinx/addendum/type-classes.rst               | 28 ++++-----------
 doc/sphinx/language/gallina-extensions.rst         | 41 +++++++++++++++++++++-
 .../language/gallina-specification-language.rst    | 40 ++++++---------------
 3 files changed, 56 insertions(+), 53 deletions(-)

diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index a463a73bef..8e6f85fca3 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -146,10 +146,12 @@ database.
 Sections and contexts
 ---------------------
 
-To ease the parametrization of developments by typeclasses, we provide a new
-way to introduce variables into section contexts, compatible with the implicit
-argument mechanism. The new command works similarly to the :cmd:`Variables`
-vernacular, except it accepts any binding context as argument. For example:
+To ease the parametrization of developments by typeclasses, one can use
+the command :cmd:`Context` to introduce variables into section contexts,
+it works similarly to the :cmd:`Variable` vernacular, except it accepts any
+binding context as argument, so variables can implicit, and
+:ref:`implicit-generalization` can be used (see also :ref:`section-mechanism`).
+For example:
 
 .. coqtop:: all
 
@@ -358,24 +360,6 @@ few other commands related to typeclasses.
    equivalent to ``Hint Resolve ident : typeclass_instances``, except it
    registers instances for :cmd:`Print Instances`.
 
-.. cmd:: Context @binders
-
-   Declare variables in the context of the current section, like :cmd:`Variable`,
-   but also allowing implicit variables and :ref:`implicit-generalization`.
-
-   .. coqdoc::
-
-       Section ContextExample.
-
-       Context {A : Type} (a b : A).
-       Context `{EqDec A}.
-
-       (* ... *)
-
-       End ContextExample.
-
-   See also :ref:`contexts`.
-
 .. tacn:: typeclasses eauto
    :name: typeclasses eauto
 
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 59506a6ff2..f2d305f4bc 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -768,7 +768,7 @@ Section :ref:`gallina-definitions`).
 .. cmd:: End @ident
 
    This command closes the section named :token:`ident`. After closing of the
-   section, the local declarations (variables and local definitions) get
+   section, the local declarations (variables and local definitions, see :cmd:`Variable`) get
    *discharged*, meaning that they stop being visible and that all global
    objects defined in the section are generalized with respect to the
    variables and local definitions they each depended on in the section.
@@ -805,6 +805,45 @@ Section :ref:`gallina-definitions`).
    Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which
    appear inside a section are canceled when the section is closed.
 
+.. cmd:: Variable @ident : @type
+
+   This command links :token:`type` to the name :token:`ident` in the context of
+   the current section (see Section :ref:`section-mechanism` for a description of
+   the section mechanism). When the current section is closed, name :token:`ident`
+   will be unknown and every object using this variable will be explicitly
+   parametrized (the variable is *discharged*).
+   The :cmd:`Variable` command out of any section is equivalent to :cmd:`Local Parameter`.
+
+   .. exn:: @ident already exists.
+      :name: @ident already exists. (Variable)
+      :undocumented:
+
+   .. cmdv:: Variable {+ @ident } : @term
+
+      Links :token:`type` to each :token:`ident`.
+
+   .. cmdv:: Variable {+ ( {+ @ident } : @term ) }
+
+      Adds blocks of variables with different specifications.
+
+   .. cmdv:: Variables {+ ( {+ @ident } : @term) }
+             Hypothesis {+ ( {+ @ident } : @term) }
+             Hypotheses {+ ( {+ @ident } : @term) }
+      :name: Variables; Hypothesis; Hypotheses
+
+      These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @term) }`.
+
+.. cmd:: Context @binders
+
+   Declare variables in the context of the current section, like :cmd:`Variable`,
+   but also allowing implicit variables and :ref:`implicit-generalization`.
+
+   .. coqdoc::
+
+     Context {A : Type} (a b : A).
+     Context `{EqDec A}.
+
+   See also :ref:`contexts` in the chapter :ref:`typeclasses`.
 
 Module system
 -------------
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 158a3f5ffc..1c6fb4b193 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -630,36 +630,16 @@ has type :token:`type`.
 
       These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`.
 
-.. cmd:: Variable @ident : @type
-
-   This command links :token:`type` to the name :token:`ident` in the context of
-   the current section (see Section :ref:`section-mechanism` for a description of
-   the section mechanism). When the current section is closed, name :token:`ident`
-   will be unknown and every object using this variable will be explicitly
-   parametrized (the variable is *discharged*). Using the :cmd:`Variable` command out
-   of any section is equivalent to using :cmd:`Local Parameter`.
-
-   See also :cmd:`Context`, a variant of :cmd:`Variable` where variables can be
-   made implicit and allowing :ref:`implicit-generalization`.
-
-   .. exn:: @ident already exists.
-      :name: @ident already exists. (Variable)
-      :undocumented:
-
-   .. cmdv:: Variable {+ @ident } : @term
-
-      Links :token:`type` to each :token:`ident`.
-
-   .. cmdv:: Variable {+ ( {+ @ident } : @term ) }
-
-      Adds blocks of variables with different specifications.
-
-   .. cmdv:: Variables {+ ( {+ @ident } : @term) }
-             Hypothesis {+ ( {+ @ident } : @term) }
-             Hypotheses {+ ( {+ @ident } : @term) }
-      :name: Variables; Hypothesis; Hypotheses
-
-      These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @term) }`.
+   .. cmdv:: Variable  {+ ( {+ @ident } : @type ) }
+             Variables {+ ( {+ @ident } : @type ) }
+             Hypothesis {+ ( {+ @ident } : @type ) }
+             Hypotheses {+ ( {+ @ident } : @type ) }
+      :name: Variable-Parameter; Variables-Parameter; Hypothesis-Parameter; Hypotheses-Parameter
+
+      Out of any section, these variants are synonyms of
+      :n:`Local Parameter {+ ( {+ @ident } : @type ) }`.
+      For their meaning inside a section, see the documentation on
+      :ref:`section-mechanism`.
 
 .. note::
    It is advised to use the commands :cmd:`Axiom`, :cmd:`Conjecture` and
-- 
cgit v1.2.3


From 94f9c0c4b6dd517dc3dca031fbcb9ff455309d19 Mon Sep 17 00:00:00 2001
From: Lysxia
Date: Sun, 17 Mar 2019 19:15:22 -0400
Subject: [Manual] Move doc on Let into Section mechanism, and more polishing

- Put "Section mechanism" example earlier
---
 doc/sphinx/addendum/type-classes.rst               | 13 +++-
 doc/sphinx/language/gallina-extensions.rst         | 91 +++++++++++++++-------
 .../language/gallina-specification-language.rst    | 43 +++++-----
 3 files changed, 89 insertions(+), 58 deletions(-)

diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 8e6f85fca3..60b346c211 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -1,7 +1,7 @@
 .. _typeclasses:
 
-Type Classes
-============
+Typeclasses
+===========
 
 This chapter presents a quick reference of the commands related to type
 classes. For an actual introduction to typeclasses, there is a
@@ -150,7 +150,7 @@ To ease the parametrization of developments by typeclasses, one can use
 the command :cmd:`Context` to introduce variables into section contexts,
 it works similarly to the :cmd:`Variable` vernacular, except it accepts any
 binding context as argument, so variables can implicit, and
-:ref:`implicit-generalization` can be used (see also :ref:`section-mechanism`).
+:ref:`implicit-generalization` can be used.
 For example:
 
 .. coqtop:: all
@@ -159,6 +159,8 @@ For example:
 
    Context `{EA : EqDec A}.
 
+.. coqtop:: in
+
    Global Program Instance option_eqb : EqDec (option A) :=
      { eqb x y := match x, y with
             | Some x, Some y => eqb x y
@@ -167,6 +169,8 @@ For example:
             end }.
    Admit Obligations.
 
+.. coqtop:: all
+
    End EqDec_defs.
 
    About option_eqb.
@@ -175,6 +179,7 @@ Here the :cmd:`Global` modifier redeclares the instance at the end of the
 section, once it has been generalized by the context variables it
 uses.
 
+.. seealso:: Section :ref:`section-mechanism`
 
 Building hierarchies
 --------------------
@@ -280,7 +285,7 @@ Summary of the commands
 .. cmd:: Class @ident {? @binders} : {? @sort} := {? @ident} { {+; @ident :{? >} @term } }
 
    The :cmd:`Class` command is used to declare a typeclass with parameters
-   ``binders`` and fields the declared record fields.
+   :token:`binders` and fields the declared record fields.
 
    .. _singleton-class:
 
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index f2d305f4bc..398ad4833d 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -754,49 +754,60 @@ used by ``Function``. A more precise description is given below.
 Section mechanism
 -----------------
 
-The sectioning mechanism can be used to to organize a proof in
-structured sections. Then local declarations become available (see
-Section :ref:`gallina-definitions`).
+Sections create local contexts which can be shared across multiple definitions.
 
+.. example::
 
-.. cmd:: Section @ident
+   Sections are opened by the :cmd:`Section` command, and closed by :cmd:`End`.
 
-   This command is used to open a section named :token:`ident`.
-   Section names do not need to be unique.
+   .. coqtop:: all
 
+      Section s1.
 
-.. cmd:: End @ident
+   Inside a section, local parameters can be introduced using :cmd:`Variable`,
+   :cmd:`Hypothesis`, or :cmd:`Context` (there are also plural variants for
+   the former two).
 
-   This command closes the section named :token:`ident`. After closing of the
-   section, the local declarations (variables and local definitions, see :cmd:`Variable`) get
-   *discharged*, meaning that they stop being visible and that all global
-   objects defined in the section are generalized with respect to the
-   variables and local definitions they each depended on in the section.
+   .. coqtop:: all
 
-   .. example::
+      Variables x y : nat.
 
-      .. coqtop:: all
+   The command :cmd:`Let` introduces section-wide :ref:`let-in`. These definitions
+   won't persist when the section is closed, and all persistent definitions which
+   depend on `y'` will be prefixed with `let y' := y in`.
 
-         Section s1.
+   .. coqtop:: in
 
-         Variables x y : nat.
+      Let y' := y.
+      Definition x' := S x.
+      Definition x'' := x' + y'.
 
-         Let y' := y.
+   .. coqtop:: all
 
-         Definition x' := S x.
+      Print x'.
+      Print x''.
 
-         Definition x'' := x' + y'.
+      End s1.
 
-         Print x'.
+      Print x'.
+      Print x''.
 
-         End s1.
+   Notice the difference between the value of :g:`x'` and :g:`x''` inside section
+   :g:`s1` and outside.
+
+.. cmd:: Section @ident
+
+   This command is used to open a section named :token:`ident`.
+   Section names do not need to be unique.
 
-         Print x'.
 
-         Print x''.
+.. cmd:: End @ident
 
-      Notice the difference between the value of :g:`x'` and :g:`x''` inside section
-      :g:`s1` and outside.
+   This command closes the section named :token:`ident`. After closing of the
+   section, the local declarations (variables and local definitions, see :cmd:`Variable`) get
+   *discharged*, meaning that they stop being visible and that all global
+   objects defined in the section are generalized with respect to the
+   variables and local definitions they each depended on in the section.
 
    .. exn:: This is not the last opened section.
       :undocumented:
@@ -808,11 +819,9 @@ Section :ref:`gallina-definitions`).
 .. cmd:: Variable @ident : @type
 
    This command links :token:`type` to the name :token:`ident` in the context of
-   the current section (see Section :ref:`section-mechanism` for a description of
-   the section mechanism). When the current section is closed, name :token:`ident`
+   the current section. When the current section is closed, name :token:`ident`
    will be unknown and every object using this variable will be explicitly
    parametrized (the variable is *discharged*).
-   The :cmd:`Variable` command out of any section is equivalent to :cmd:`Local Parameter`.
 
    .. exn:: @ident already exists.
       :name: @ident already exists. (Variable)
@@ -843,7 +852,31 @@ Section :ref:`gallina-definitions`).
      Context {A : Type} (a b : A).
      Context `{EqDec A}.
 
-   See also :ref:`contexts` in the chapter :ref:`typeclasses`.
+.. seealso:: Section :ref:`contexts` in chapter :ref:`typeclasses`.
+
+.. cmd:: Let @ident := @term
+
+   This command binds the value :token:`term` to the name :token:`ident` in the
+   environment of the current section. The name :token:`ident` disappears when the
+   current section is eventually closed, and all persistent definitions and
+   theorems within the section and depending on :token:`ident` are
+   prefixed by the let-in definition :n:`let @ident := @term in`.
+
+   .. exn:: @ident already exists.
+      :name: @ident already exists. (Let)
+      :undocumented:
+
+   .. cmdv:: Let @ident {? @binders } {? : @type } := @term
+      :undocumented:
+
+   .. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body}
+      :name: Let Fixpoint
+      :undocumented:
+
+   .. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body}
+      :name: Let CoFixpoint
+      :undocumented:
+
 
 Module system
 -------------
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 1c6fb4b193..67e59768d6 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -634,13 +634,18 @@ has type :token:`type`.
              Variables {+ ( {+ @ident } : @type ) }
              Hypothesis {+ ( {+ @ident } : @type ) }
              Hypotheses {+ ( {+ @ident } : @type ) }
-      :name: Variable-Parameter; Variables-Parameter; Hypothesis-Parameter; Hypotheses-Parameter
+      :name: Variable (outside a section); Variables (outside a section); Hypothesis (outside a section); Hypotheses (outside a section)
 
       Out of any section, these variants are synonyms of
       :n:`Local Parameter {+ ( {+ @ident } : @type ) }`.
-      For their meaning inside a section, see the documentation on
+      For their meaning inside a section, see :cmd:`Variable` in
       :ref:`section-mechanism`.
 
+      .. warn:: @ident is declared as a local axiom [local-declaration,scope]
+
+         Warning that is emitted when using :cmd:`Variable` instead of
+         :cmd:`Local Parameter`.
+
 .. note::
    It is advised to use the commands :cmd:`Axiom`, :cmd:`Conjecture` and
    :cmd:`Hypothesis` (and their plural forms) for logical postulates (i.e. when
@@ -648,6 +653,8 @@ has type :token:`type`.
    :cmd:`Parameter` and :cmd:`Variable` (and their plural forms) in other cases
    (corresponding to the declaration of an abstract mathematical entity).
 
+.. seealso:: Section :ref:`section-mechanism`.
+
 .. _gallina-definitions:
 
 Definitions
@@ -704,32 +711,18 @@ Section :ref:`typing-rules`.
 
       This is equivalent to :cmd:`Definition`.
 
-.. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`.
-
-.. cmd:: Let @ident := @term
-
-   This command binds the value :token:`term` to the name :token:`ident` in the
-   environment of the current section. The name :token:`ident` disappears when the
-   current section is eventually closed, and all persistent objects (such
-   as theorems) defined within the section and depending on :token:`ident` are
-   prefixed by the let-in definition :n:`let @ident := @term in`.
-   Using the :cmd:`Let` command out of any section is equivalent to using
-   :cmd:`Local Definition`.
-
-   .. exn:: @ident already exists.
-      :name: @ident already exists. (Let)
-      :undocumented:
+   .. cmdv:: Let @ident := @term
+      :name: Let (outside a section)
 
-   .. cmdv:: Let @ident {? @binders } {? : @type } := @term
-      :undocumented:
+      Out of any section, this variant is a synonym of
+      :n:`Local Definition @ident := @term`.
+      For its meaning inside a section, see :cmd:`Let` in
+      :ref:`section-mechanism`.
 
-   .. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body}
-      :name: Let Fixpoint
-      :undocumented:
+      .. warn:: @ident is declared as a local definition [local-declaration,scope]
 
-   .. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body}
-      :name: Let CoFixpoint
-      :undocumented:
+         Warning that is emitted when using :cmd:`Let` instead of
+         :cmd:`Local Definition`.
 
 .. seealso:: Section :ref:`section-mechanism`, commands :cmd:`Opaque`,
              :cmd:`Transparent`, and tactic :tacn:`unfold`.
-- 
cgit v1.2.3


From b64dc640d2af26b1ccf2524c1050c16f57d2be35 Mon Sep 17 00:00:00 2001
From: Lysxia
Date: Mon, 18 Mar 2019 08:20:10 -0400
Subject: [Manual] Move command Context after Let, and more polishing

- Refine some `@term` into `@type`
---
 doc/sphinx/addendum/type-classes.rst               |  8 ++--
 doc/sphinx/language/gallina-extensions.rst         | 51 +++++++++++-----------
 .../language/gallina-specification-language.rst    | 12 ++---
 3 files changed, 36 insertions(+), 35 deletions(-)

diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 60b346c211..e6a5b3972c 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -146,10 +146,10 @@ database.
 Sections and contexts
 ---------------------
 
-To ease the parametrization of developments by typeclasses, one can use
-the command :cmd:`Context` to introduce variables into section contexts,
-it works similarly to the :cmd:`Variable` vernacular, except it accepts any
-binding context as argument, so variables can implicit, and
+To ease developments parameterized by many instances, one can use the
+:cmd:`Context` command to introduce these parameters into section contexts,
+it works similarly to the command :cmd:`Variable`, except it accepts any
+binding context as an argument, so variables can be implicit, and
 :ref:`implicit-generalization` can be used.
 For example:
 
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 398ad4833d..497504e706 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -766,7 +766,7 @@ Sections create local contexts which can be shared across multiple definitions.
 
    Inside a section, local parameters can be introduced using :cmd:`Variable`,
    :cmd:`Hypothesis`, or :cmd:`Context` (there are also plural variants for
-   the former two).
+   the first two).
 
    .. coqtop:: all
 
@@ -827,40 +827,28 @@ Sections create local contexts which can be shared across multiple definitions.
       :name: @ident already exists. (Variable)
       :undocumented:
 
-   .. cmdv:: Variable {+ @ident } : @term
+   .. cmdv:: Variable {+ @ident } : @type
 
       Links :token:`type` to each :token:`ident`.
 
-   .. cmdv:: Variable {+ ( {+ @ident } : @term ) }
+   .. cmdv:: Variable {+ ( {+ @ident } : @type ) }
 
-      Adds blocks of variables with different specifications.
+      Declare one or more variables with various types.
 
-   .. cmdv:: Variables {+ ( {+ @ident } : @term) }
-             Hypothesis {+ ( {+ @ident } : @term) }
-             Hypotheses {+ ( {+ @ident } : @term) }
+   .. cmdv:: Variables {+ ( {+ @ident } : @type) }
+             Hypothesis {+ ( {+ @ident } : @type) }
+             Hypotheses {+ ( {+ @ident } : @type) }
       :name: Variables; Hypothesis; Hypotheses
 
-      These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @term) }`.
-
-.. cmd:: Context @binders
-
-   Declare variables in the context of the current section, like :cmd:`Variable`,
-   but also allowing implicit variables and :ref:`implicit-generalization`.
-
-   .. coqdoc::
-
-     Context {A : Type} (a b : A).
-     Context `{EqDec A}.
-
-.. seealso:: Section :ref:`contexts` in chapter :ref:`typeclasses`.
+      These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`.
 
 .. cmd:: Let @ident := @term
 
    This command binds the value :token:`term` to the name :token:`ident` in the
-   environment of the current section. The name :token:`ident` disappears when the
-   current section is eventually closed, and all persistent definitions and
-   theorems within the section and depending on :token:`ident` are
-   prefixed by the let-in definition :n:`let @ident := @term in`.
+   environment of the current section. The name :token:`ident` is accessible
+   only within the current section. When the section is closed, all persistent
+   definitions and theorems within it and depending on :token:`ident`
+   will be prefixed by the let-in definition :n:`let @ident := @term in`.
 
    .. exn:: @ident already exists.
       :name: @ident already exists. (Let)
@@ -877,6 +865,19 @@ Sections create local contexts which can be shared across multiple definitions.
       :name: Let CoFixpoint
       :undocumented:
 
+.. cmd:: Context @binders
+
+   Declare variables in the context of the current section, like :cmd:`Variable`,
+   but also allowing implicit variables, :ref:`implicit-generalization`, and
+   let-binders.
+
+   .. coqdoc::
+
+     Context {A : Type} (a b : A).
+     Context `{EqDec A}.
+     Context (b' := b).
+
+.. seealso:: Section :ref:`binders`. Section :ref:`contexts` in chapter :ref:`typeclasses`.
 
 Module system
 -------------
@@ -2100,7 +2101,7 @@ or :g:`m` to the type :g:`nat` of natural numbers).
 
   This is useful for declaring the implicit type of a single variable.
 
-.. cmdv:: Implicit Types {+ ( {+ @ident } : @term ) }
+.. cmdv:: Implicit Types {+ ( {+ @ident } : @type ) }
 
   Adds blocks of implicit types with different specifications.
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 67e59768d6..e67f53c950 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -636,14 +636,14 @@ has type :token:`type`.
              Hypotheses {+ ( {+ @ident } : @type ) }
       :name: Variable (outside a section); Variables (outside a section); Hypothesis (outside a section); Hypotheses (outside a section)
 
-      Out of any section, these variants are synonyms of
+      Outside of any section, these variants are synonyms of
       :n:`Local Parameter {+ ( {+ @ident } : @type ) }`.
       For their meaning inside a section, see :cmd:`Variable` in
       :ref:`section-mechanism`.
 
       .. warn:: @ident is declared as a local axiom [local-declaration,scope]
 
-         Warning that is emitted when using :cmd:`Variable` instead of
+         Warning generated when using :cmd:`Variable` instead of
          :cmd:`Local Parameter`.
 
 .. note::
@@ -694,10 +694,10 @@ Section :ref:`typing-rules`.
       .. exn:: The term @term has type @type while it is expected to have type @type'.
          :undocumented:
 
-   .. cmdv:: Definition @ident @binders {? : @term } := @term
+   .. cmdv:: Definition @ident @binders {? : @type } := @term
 
       This is equivalent to
-      :n:`Definition @ident : forall @binders, @term := fun @binders => @term`.
+      :n:`Definition @ident : forall @binders, @type := fun @binders => @term`.
 
    .. cmdv:: Local Definition @ident {? @binders } {? : @type } := @term
       :name: Local Definition
@@ -714,14 +714,14 @@ Section :ref:`typing-rules`.
    .. cmdv:: Let @ident := @term
       :name: Let (outside a section)
 
-      Out of any section, this variant is a synonym of
+      Outside of any section, this variant is a synonym of
       :n:`Local Definition @ident := @term`.
       For its meaning inside a section, see :cmd:`Let` in
       :ref:`section-mechanism`.
 
       .. warn:: @ident is declared as a local definition [local-declaration,scope]
 
-         Warning that is emitted when using :cmd:`Let` instead of
+         Warning generated when using :cmd:`Let` instead of
          :cmd:`Local Definition`.
 
 .. seealso:: Section :ref:`section-mechanism`, commands :cmd:`Opaque`,
-- 
cgit v1.2.3


From e7ddf978adbf441d34b8c17502caaa05ee8da04b Mon Sep 17 00:00:00 2001
From: Lysxia
Date: Mon, 18 Mar 2019 08:20:10 -0400
Subject: [Manual] Parametrize -> ParametErize

- Refine some `@term` into `@type`
---
 doc/sphinx/language/gallina-extensions.rst             |  2 +-
 doc/sphinx/language/gallina-specification-language.rst | 10 +++++-----
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 497504e706..18cafd1f21 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -821,7 +821,7 @@ Sections create local contexts which can be shared across multiple definitions.
    This command links :token:`type` to the name :token:`ident` in the context of
    the current section. When the current section is closed, name :token:`ident`
    will be unknown and every object using this variable will be explicitly
-   parametrized (the variable is *discharged*).
+   parameterized (the variable is *discharged*).
 
    .. exn:: @ident already exists.
       :name: @ident already exists. (Variable)
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index e67f53c950..8a5e9d87f8 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -853,8 +853,8 @@ which is a type whose conclusion is a sort.
    successor :g:`(S (S n))` satisfies also :g:`P`. This is indeed analogous to the
    structural induction principle we got for :g:`nat`.
 
-Parametrized inductive types
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Parameterized inductive types
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. cmdv:: Inductive @ident @binders {? : @type } := {? | } @ident : @type {* | @ident : @type}
 
@@ -930,7 +930,7 @@ Parametrized inductive types
      because the conclusion of the type of constructors should be :g:`listw A`
      in both cases.
 
-   + A parametrized inductive definition can be defined using annotations
+   + A parameterized inductive definition can be defined using annotations
      instead of parameters but it will sometimes give a different (bigger)
      sort for the inductive definition and will produce a less convenient
      rule for case elimination.
@@ -990,7 +990,7 @@ Mutually defined inductive types
 
    .. cmdv:: Inductive @ident @binders {? : @type } := {? | } {*| @ident : @type } {* with {? | } {*| @ident @binders {? : @type } } }
 
-      In this variant, the inductive definitions are parametrized
+      In this variant, the inductive definitions are parameterized
       with :token:`binders`. However, parameters correspond to a local context
       in which the whole set of inductive declarations is done. For this
       reason, the parameters must be strictly the same for each inductive types.
@@ -1026,7 +1026,7 @@ Mutually defined inductive types
 
       Check forest_rec.
 
-   Assume we want to parametrize our mutual inductive definitions with the
+   Assume we want to parameterize our mutual inductive definitions with the
    two type variables :g:`A` and :g:`B`, the declaration should be
    done the following way:
 
-- 
cgit v1.2.3