Move 'new in Coq 8.1' subsection to an appropriate place.

1 files changed, 34 insertions, 37 deletions

diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index c4987a8f7..85e4e8e1f 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -870,59 +870,56 @@ Parametrized inductive types
 
          Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A).
 
-Variants
-~~~~~~~~
+.. note::
+   + It is possible in the type of a constructor, to
+     invoke recursively the inductive definition on an argument which is not
+     the parameter itself.
 
-.. cmd:: Variant @ident @binders {? : @type } := {? | } @ident : @type {* | @ident : @type}
+     One can define :
 
-   The :cmd:`Variant` command is identical to the :cmd:`Inductive` command, except
-   that it disallows recursive definition of types (for instance, lists cannot
-   be defined using :cmd:`Variant`). No induction scheme is generated for
-   this variant, unless option :opt:`Nonrecursive Elimination Schemes` is on.
-
-   .. exn:: The @num th argument of @ident must be @ident in @type.
-      :undocumented:
+     .. coqtop:: all
 
-New from Coq V8.1
-+++++++++++++++++
+        Inductive list2 (A:Set) : Set :=
+        | nil2 : list2 A
+        | cons2 : A -> list2 (A*A) -> list2 A.
 
-The condition on parameters for inductive definitions has been relaxed
-since Coq V8.1. It is now possible in the type of a constructor, to
-invoke recursively the inductive definition on an argument which is not
-the parameter itself.
+     that can also be written by specifying only the type of the arguments:
 
-One can define :
+     .. coqtop:: all reset
 
-.. coqtop:: all
+        Inductive list2 (A:Set) : Set := nil2 | cons2 (_:A) (_:list2 (A*A)).
 
-   Inductive list2 (A:Set) : Set :=
-   | nil2 : list2 A
-   | cons2 : A -> list2 (A*A) -> list2 A.
+     But the following definition will give an error:
 
-that can also be written by specifying only the type of the arguments:
+     .. coqtop:: all
 
-.. coqtop:: all reset
+        Fail Inductive listw (A:Set) : Set :=
+        | nilw : listw (A*A)
+        | consw : A -> listw (A*A) -> listw (A*A).
 
-   Inductive list2 (A:Set) : Set := nil2 | cons2 (_:A) (_:list2 (A*A)).
+     because the conclusion of the type of constructors should be :g:`listw A`
+     in both cases.
 
-But the following definition will give an error:
+   + A parametrized 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.
 
-.. coqtop:: all
+.. seealso::
+   Section :ref:`inductive-definitions` and the :tacn:`induction` tactic.
 
-   Fail Inductive listw (A:Set) : Set :=
-   | nilw : listw (A*A)
-   | consw : A -> listw (A*A) -> listw (A*A).
+Variants
+~~~~~~~~
 
-Because the conclusion of the type of constructors should be :g:`listw A` in
-both cases.
+.. cmd:: Variant @ident @binders {? : @type } := {? | } @ident : @type {* | @ident : @type}
 
-A parametrized 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.
+   The :cmd:`Variant` command is identical to the :cmd:`Inductive` command, except
+   that it disallows recursive definition of types (for instance, lists cannot
+   be defined using :cmd:`Variant`). No induction scheme is generated for
+   this variant, unless option :opt:`Nonrecursive Elimination Schemes` is on.
 
-See also Section :ref:`inductive-definitions` and the :tacn:`induction`
-tactic.
+   .. exn:: The @num th argument of @ident must be @ident in @type.
+      :undocumented:
 
 Mutually defined inductive types
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~