Merge sections on Variants and Private inductive types into new file.

1 files changed, 29 insertions, 1 deletions

diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst
index ff4212bdd4..d8fba5bc3d 100644
--- a/doc/sphinx/language/core/variants.rst
+++ b/doc/sphinx/language/core/variants.rst
@@ -1,5 +1,8 @@
+Variants and the `match` construct
+==================================
+
 Variants
-~~~~~~~~
+--------
 
 .. cmd:: Variant @variant_definition {* with @variant_definition }
 
@@ -21,3 +24,28 @@ Variants
 
    .. exn:: The @num th argument of @ident must be @ident in @type.
       :undocumented:
+
+Private (matching) inductive types
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. attr:: private(matching)
+
+   This attribute can be used to forbid the use of the :g:`match`
+   construct on objects of this inductive type outside of the module
+   where it is defined.  There is also a legacy syntax using the
+   ``Private`` prefix (cf. :n:`@legacy_attr`).
+
+   The main use case of private (matching) inductive types is to emulate
+   quotient types / higher-order inductive types in projects such as
+   the `HoTT library <https://github.com/HoTT/HoTT>`_.
+
+.. example::
+
+   .. coqtop:: all
+
+      Module Foo.
+      #[ private(matching) ] Inductive my_nat := my_O : my_nat | my_S : my_nat -> my_nat.
+      Check (fun x : my_nat => match x with my_O => true | my_S _ => false end).
+      End Foo.
+      Import Foo.
+      Fail Check (fun x : my_nat => match x with my_O => true | my_S _ => false end).