2 files changed, 75 insertions, 0 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/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
 *****************