Merge remote-tracking branch 'origin/master' into stm+doc_hook

6 files changed, 40 insertions, 51 deletions

diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst
index dd21ea09bd..b593b0cef1 100644
--- a/doc/sphinx/addendum/canonical-structures.rst
+++ b/doc/sphinx/addendum/canonical-structures.rst
@@ -209,7 +209,7 @@ We need to define a new class that inherits from both ``EQ`` and ``LE``.
                         LE_class : LE.class T;
                         extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }.
 
-    Structure type := _Pack { obj : Type; class_of : class obj }.
+    Structure type := _Pack { obj : Type; #[canonical(false)] class_of : class obj }.
 
     Arguments Mixin {e le} _.
 
@@ -219,6 +219,9 @@ The mixin component of the ``LEQ`` class contains all the extra content we
 are adding to ``EQ`` and ``LE``. In particular it contains the requirement
 that the two relations we are combining are compatible.
 
+The `class_of` projection of the `type` structure is annotated as *not canonical*;
+it plays no role in the search for instances.
+
 Unfortunately there is still an obstacle to developing the algebraic
 theory of this new class.
 
@@ -313,9 +316,7 @@ constructor ``*``. It also tests that they work as expected.
 Unfortunately, these declarations are very verbose. In the following
 subsection we show how to make them more compact.
 
-.. FIXME shouldn't warn
-
-.. coqtop:: all warn
+.. coqtop:: all
 
   Module Add_instance_attempt.
 
@@ -420,9 +421,7 @@ the reader can refer to :cite:`CSwcu`.
 
 The declaration of canonical instances can now be way more compact:
 
-.. FIXME should not warn
-
-.. coqtop:: all warn
+.. coqtop:: all
 
   Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx.
   
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index e93b01f14d..8a895eb515 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -99,7 +99,7 @@ Extraction Options
 Setting the target language
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Extraction Language ( OCaml | Haskell | Scheme )
+.. cmd:: Extraction Language {| OCaml | Haskell | Scheme }
    :name: Extraction Language
 
    The ability to fix target language is the first and more important
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index b474c51f17..847abb33fc 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -170,12 +170,12 @@ compatibility constraints.
 Adding new relations and morphisms
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd::  Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by refl} {? symmetry proved by sym} {? transitivity proved by trans} as @ident
+.. cmd::  Add Parametric Relation @binders : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by @term} {? symmetry proved by @term} {? transitivity proved by @term} as @ident
 
    This command declares a parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm)`,
    :g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)`.
 
-   The :token:`ident` gives a unique name to the morphism and it is used
+   The final :token:`ident` gives a unique name to the morphism and it is used
    by the command to generate fresh names for automatically provided
    lemmas used internally.
 
@@ -219,15 +219,16 @@ replace terms with related ones only in contexts that are syntactic
 compositions of parametric morphism instances declared with the
 following command.
 
-.. cmd:: Add Parametric Morphism (x1 : T1) ... (xk : Tk) : (f t1 ... tn) with signature sig as @ident
+.. cmd:: Add Parametric Morphism @binders : (@ident {+ @term__1}) with signature @term__2 as @ident
 
-   This command declares ``f`` as a parametric morphism of signature ``sig``. The
-   identifier :token:`ident` gives a unique name to the morphism and it is used as
-   the base name of the typeclass instance definition and as the name of
-   the lemma that proves the well-definedness of the morphism. The
-   parameters of the morphism as well as the signature may refer to the
-   context of variables. The command asks the user to prove interactively
-   that ``f`` respects the relations identified from the signature.
+   This command declares a parametric morphism :n:`@ident {+ @term__1}` of
+   signature :n:`@term__2`.  The final identifier :token:`ident` gives a unique
+   name to the morphism and it is used as the base name of the typeclass
+   instance definition and as the name of the lemma that proves the
+   well-definedness of the morphism. The parameters of the morphism as well as
+   the signature may refer to the context of variables. The command asks the
+   user to prove interactively that the function denoted by the first
+   :token:`ident` respects the relations identified from the signature.
 
 .. example::
 
@@ -577,7 +578,7 @@ Deprecated syntax and backward incompatibilities
    Notice that the syntax is not completely backward compatible since the
    identifier was not required.
 
-.. cmd:: Add Morphism f : @ident
+.. cmd:: Add Morphism @ident : @ident
    :name: Add Morphism
 
    This command is restricted to the declaration of morphisms
@@ -809,7 +810,7 @@ Usage
 ~~~~~
 
 
-.. tacn:: rewrite_strat @s [in @ident]
+.. tacn:: rewrite_strat @s {? in @ident }
    :name: rewrite_strat
 
    Rewrite using the strategy s in hypothesis ident or the conclusion.
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index b410833d25..22ddcae584 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -283,7 +283,7 @@ optional identifier is used when multiple functions have unsolved
 obligations (e.g. when defining mutually recursive blocks). The
 optional tactic is replaced by the default one if not specified.
 
-.. cmd:: {? Local|Global} Obligation Tactic := @tactic
+.. cmd:: {? {| Local | Global } } Obligation Tactic := @tactic
    :name: Obligation Tactic
 
    Sets the default obligation solving tactic applied to all obligations
diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
index c0c8c2d79c..8935ba27e3 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -10,9 +10,9 @@ SProp (proof irrelevant propositions)
 This section describes the extension of |Coq| with definitionally
 proof irrelevant propositions (types in the sort :math:`\SProp`, also
 known as strict propositions). To use :math:`\SProp` you must pass
-``-allow-sprop`` to the |Coq| program or use :opt:`Allow StrictProp`.
+``-allow-sprop`` to the |Coq| program or use :flag:`Allow StrictProp`.
 
-.. opt:: Allow StrictProp
+.. flag:: Allow StrictProp
    :name: Allow StrictProp
 
    Allows using :math:`\SProp` when set and forbids it when unset. The
@@ -201,10 +201,10 @@ This means that some errors will be delayed until ``Qed``:
 
    Abort.
 
-.. opt:: Elaboration StrictProp Cumulativity
+.. flag:: Elaboration StrictProp Cumulativity
    :name: Elaboration StrictProp Cumulativity
 
-   Unset this option (it's on by default) to be strict with regard to
+   Unset this flag (it is on by default) to be strict with regard to
    :math:`\SProp` cumulativity during elaboration.
 
 The implementation of proof irrelevance uses inferred "relevance"
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index a5e9023732..65934efaa6 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -311,24 +311,24 @@ Summary of the commands
 
          This command has no effect when used on a typeclass.
 
-.. cmd:: Instance @ident {? @binders} : @class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi }
+.. cmd:: Instance @ident {? @binders} : @term__0 {+ @term} {? | @num} := { {*; @field_def} }
 
    This command is used to declare a typeclass instance named
-   :token:`ident` of the class :token:`class` with parameters ``t1`` to ``tn`` and
-   fields ``b1`` to ``bi``, where each field must be a declared field of
-   the class.  Missing fields must be filled in interactive proof mode.
+   :token:`ident` of the class :n:`@term__0` with parameters :token:`term` and
+   fields defined by :token:`field_def`, where each field must be a declared field of
+   the class.
 
    An arbitrary context of :token:`binders` can be put after the name of the
    instance and before the colon to declare a parameterized instance. An
    optional priority can be declared, 0 being the highest priority as for
-   :tacn:`auto` hints. If the priority is not specified, it defaults to the number
+   :tacn:`auto` hints. If the priority :token:`num` 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}, @term__0 {+ @term} {? | @num } := @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
+      for directly giving an explicit term of type :n:`forall @binders, @term__0
+      {+ @term}`.  One need not even mention the unique field name for
       singleton classes.
 
    .. cmdv:: Global Instance
@@ -356,11 +356,11 @@ Summary of the commands
 Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a
 few other commands related to typeclasses.
 
-.. cmd:: Existing Instance {+ @ident} [| priority]
+.. cmd:: Existing Instance {+ @ident} {? | @num}
 
    This command adds an arbitrary list of constants whose type ends with
    an applied typeclass to the instance database with an optional
-   priority.  It can be used for redeclaring instances at the end of
+   priority :token:`num`.  It can be used for redeclaring instances at the end of
    sections, or declaring structure projections as instances. This is
    equivalent to ``Hint Resolve ident : typeclass_instances``, except it
    registers instances for :cmd:`Print Instances`.
@@ -405,8 +405,10 @@ few other commands related to typeclasses.
      resolution with the local hypotheses use full conversion during
      unification.
 
+   + When considering local hypotheses, we use the union of all the modes
+     declared in the given databases.
 
-   .. cmdv:: typeclasses eauto @num
+   .. tacv:: typeclasses eauto @num
 
       .. warning::
          The semantics for the limit :n:`@num`
@@ -415,7 +417,7 @@ few other commands related to typeclasses.
          counted, which might result in larger limits being necessary when
          searching with ``typeclasses eauto`` than with :tacn:`auto`.
 
-   .. cmdv:: typeclasses eauto with {+ @ident}
+   .. tacv:: typeclasses eauto with {+ @ident}
 
       This variant runs resolution with the given hint databases. It treats
       typeclass subgoals the same as other subgoals (no shelving of
@@ -561,23 +563,10 @@ Settings
    of goals.  Setting this option to 1 or 2 turns on :flag:`Typeclasses Debug`; setting this
    option to 0 turns that option off.
 
-.. flag:: Refine Instance Mode
-
-   .. deprecated:: 8.10
-
-   This flag allows to switch the behavior of instance declarations made through
-   the Instance command.
-
-   + When it is off (the default), they fail with an error instead.
-
-   + When it is on, instances that have unsolved holes in
-     their proof-term silently open the proof mode with the remaining
-     obligations to prove.
-
 Typeclasses eauto `:=`
 ~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Typeclasses eauto := {? debug} {? (dfs) | (bfs) } @num
+.. cmd:: Typeclasses eauto := {? debug} {? {| (dfs) | (bfs) } } @num
    :name: Typeclasses eauto
 
    This command allows more global customization of the typeclass