7 files changed, 105 insertions, 12 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index c08a9ed0e6..6410620b40 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1046,6 +1046,67 @@ between universes for inductive types in the Type hierarchy.
       exT_intro : forall X:Type, P X -> exType P.
 
 
+.. example:: Negative occurrence (first example)
+
+   The following inductive definition is rejected because it does not
+   satisfy the positivity condition:
+
+   .. coqtop:: all
+
+      Fail Inductive I : Prop := not_I_I (not_I : I -> False) : I.
+
+   If we were to accept such definition, we could derive a
+   contradiction from it (we can test this by disabling the
+   :flag:`Positivity Checking` flag):
+
+   .. coqtop:: none
+
+      Unset Positivity Checking.
+      Inductive I : Prop := not_I_I (not_I : I -> False) : I.
+      Set Positivity Checking.
+
+   .. coqtop:: all
+
+      Definition I_not_I : I -> ~ I := fun i =>
+        match i with not_I_I not_I => not_I end.
+
+   .. coqtop:: in
+
+      Lemma contradiction : False.
+      Proof.
+        enough (I /\ ~ I) as [] by contradiction.
+        split.
+        - apply not_I_I.
+          intro.
+          now apply I_not_I.
+        - intro.
+          now apply I_not_I.
+      Qed.
+
+.. example:: Negative occurrence (second example)
+
+   Here is another example of an inductive definition which is
+   rejected because it does not satify the positivity condition:
+
+   .. coqtop:: all
+
+      Fail Inductive Lam := lam (_ : Lam -> Lam).
+
+   Again, if we were to accept it, we could derive a contradiction
+   (this time through a non-terminating recursive function):
+
+   .. coqtop:: none
+
+      Unset Positivity Checking.
+      Inductive Lam := lam (_ : Lam -> Lam).
+      Set Positivity Checking.
+
+   .. coqtop:: all
+
+      Fixpoint infinite_loop l : False :=
+        match l with lam x => infinite_loop (x l) end.
+
+      Check infinite_loop (lam (@id Lam)) : False.
 
 .. _Template-polymorphism:
 
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index f477bf239d..f50cf9340c 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1927,9 +1927,11 @@ Renaming implicit arguments
 
    This command is used to redefine the names of implicit arguments.
 
-With the assert flag, ``Arguments`` can be used to assert that a given
-object has the expected number of arguments and that these arguments
-are named as expected.
+.. cmd:: Arguments @qualid {* @name} : assert
+   :name: Arguments (assert)
+
+   This command is used to assert that a given object has the expected
+   number of arguments and that these arguments are named as expected.
 
 .. example:: (continued)
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index ae9d284661..dd65d4aeb3 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1556,6 +1556,11 @@ the following attributes names are recognized:
           now foo.
         Abort.
 
+.. warn:: Unsupported attribute
+
+   This warning is an error by default. It is caused by using a
+   command with some attribute it does not understand.
+
 .. [1]
    This is similar to the expression “*entry* :math:`\{` sep *entry*
    :math:`\}`” in standard BNF, or “*entry* :math:`(` sep *entry*
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 79eddbd3b5..6efc634087 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -516,7 +516,9 @@ Coq provides a derived tactic to check that a tactic *fails*:
 .. tacn:: assert_fails @ltac_expr
    :name: assert_fails
 
-   This behaves like :n:`tryif @ltac_expr then fail 0 tac "succeeds" else idtac`.
+   This behaves like :tacn:`idtac` if :n:`@ltac_expr` fails, and
+   behaves like :n:`fail 0 @ltac_expr "succeeds"` if :n:`@ltac_expr`
+   has at least one success.
 
 Checking the success
 ~~~~~~~~~~~~~~~~~~~~
@@ -528,7 +530,7 @@ success:
    :name: assert_succeeds
 
    This behaves like
-   :n:`tryif (assert_fails tac) then fail 0 tac "fails" else idtac`.
+   :n:`tryif (assert_fails @ltac_expr) then fail 0 @ltac_expr "fails" else idtac`.
 
 Solving
 ~~~~~~~
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 18d2c79461..cfdc70d50e 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -563,6 +563,20 @@ for it.
 - `&x` as a Coq constr expression expands to
   `ltac2:(Control.refine (fun () => hyp @x))`.
 
+In the special case where Ltac2 antiquotations appear inside a Coq term
+notation, the notation variables are systematically bound in the body
+of the tactic expression with type `Ltac2.Init.preterm`. Such a type represents
+untyped syntactic Coq expressions, which can by typed in the
+current context using the `Ltac2.Constr.pretype` function.
+
+.. example::
+
+   The following notation is essentially the identity.
+
+   .. coqtop:: in
+
+      Notation "[ x ]" := ltac2:(let x := Ltac2.Constr.pretype x in exact $x) (only parsing).
+
 Dynamic semantics
 *****************
 
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 57a54bc0ad..00f8269dc3 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -535,7 +535,7 @@ Requesting information
             eexists ?[n].
             Show n.
 
-   .. cmdv:: Show Proof
+   .. cmdv:: Show Proof {? Diffs {? removed } }
       :name: Show Proof
 
       Displays the proof term generated by the tactics
@@ -544,6 +544,12 @@ Requesting information
       constructed. Each hole is an existential variable, which appears as a
       question mark followed by an identifier.
 
+      Experimental: Specifying “Diffs” highlights the difference between the
+      current and previous proof step.  By default, the command shows the
+      output once with additions highlighted.  Including “removed” shows
+      the output twice: once showing removals and once showing additions.
+      It does not examine the :opt:`Diffs` option.  See :ref:`showing_diffs`.
+
    .. cmdv:: Show Conjectures
       :name: Show Conjectures
 
@@ -624,8 +630,11 @@ Showing differences between proof steps
 ---------------------------------------
 
 
-Coq can automatically highlight the differences between successive proof steps and between
-values in some error messages.
+Coq can automatically highlight the differences between successive proof steps
+and between values in some error messages.  Also, as an experimental feature,
+Coq can also highlight differences between proof steps shown in the :cmd:`Show Proof`
+command, but only, for now, when using coqtop and Proof General.
+
 For example, the following screenshots of CoqIDE and coqtop show the application
 of the same :tacn:`intros` tactic.  The tactic creates two new hypotheses, highlighted in green.
 The conclusion is entirely in pale green because although it’s changed, no tokens were added
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index a28ce600ca..02910e603a 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1442,8 +1442,8 @@ Numeral notations
      of the resulting term will be refreshed.
 
      Note that only fully-reduced ground terms (terms containing only
-     function application, constructors, inductive type families, and
-     primitive integers) will be considered for printing.
+     function application, constructors, inductive type families,
+     sorts, and primitive integers) will be considered for printing.
 
    .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num).
 
@@ -1592,8 +1592,8 @@ String notations
      of the resulting term will be refreshed.
 
      Note that only fully-reduced ground terms (terms containing only
-     function application, constructors, inductive type families, and
-     primitive integers) will be considered for printing.
+     function application, constructors, inductive type families,
+     sorts, and primitive integers) will be considered for printing.
 
    .. exn:: Cannot interpret this string as a value of type @type