[Ada] Remove SPARK containers from GNAT documentation

This patch removes documentation on the SPARK containers,
now under the spark2014 repository.

gcc/ada/

	* doc/gnat_rm/the_gnat_library.rst: Remove paragraphs about SPARK
	containers.
	* gnat_rm.texi, gnat_ugn.texi: Regenerate.

1 files changed, 0 insertions, 219 deletions

diff --git a/gcc/ada/doc/gnat_rm/the_gnat_library.rst b/gcc/ada/doc/gnat_rm/the_gnat_library.rst
index 524e3e0..d791f81 100644
--- a/gcc/ada/doc/gnat_rm/the_gnat_library.rst
+++ b/gcc/ada/doc/gnat_rm/the_gnat_library.rst
@@ -120,225 +120,6 @@ instead of ``Character``.  The provision of such a package
 is specifically authorized by the Ada Reference Manual
 (RM A.3.3(27)).
 
-.. _`Ada.Containers.Formal_Doubly_Linked_Lists_(a-cfdlli.ads)`:
-
-``Ada.Containers.Formal_Doubly_Linked_Lists`` (:file:`a-cfdlli.ads`)
-====================================================================
-
-.. index:: Ada.Containers.Formal_Doubly_Linked_Lists (a-cfdlli.ads)
-
-.. index:: Formal container for doubly linked lists
-
-This child of ``Ada.Containers`` defines a modified version of the
-Ada 2005 container for doubly linked lists, meant to facilitate formal
-verification of code using such containers. The specification of this
-unit is compatible with SPARK 2014.
-
-Note that although this container was designed with formal verification
-in mind, it may well be generally useful in that it is a simplified more
-efficient version than the one defined in the standard. In particular it
-does not have the complex overhead required to detect cursor tampering.
-
-.. _`Ada.Containers.Formal_Hashed_Maps_(a-cfhama.ads)`:
-
-``Ada.Containers.Formal_Hashed_Maps`` (:file:`a-cfhama.ads`)
-============================================================
-
-.. index:: Ada.Containers.Formal_Hashed_Maps (a-cfhama.ads)
-
-.. index:: Formal container for hashed maps
-
-This child of ``Ada.Containers`` defines a modified version of the
-Ada 2005 container for hashed maps, meant to facilitate formal
-verification of code using such containers. The specification of this
-unit is compatible with SPARK 2014.
-
-Note that although this container was designed with formal verification
-in mind, it may well be generally useful in that it is a simplified more
-efficient version than the one defined in the standard. In particular it
-does not have the complex overhead required to detect cursor tampering.
-
-.. _`Ada.Containers.Formal_Hashed_Sets_(a-cfhase.ads)`:
-
-``Ada.Containers.Formal_Hashed_Sets`` (:file:`a-cfhase.ads`)
-============================================================
-
-.. index:: Ada.Containers.Formal_Hashed_Sets (a-cfhase.ads)
-
-.. index:: Formal container for hashed sets
-
-This child of ``Ada.Containers`` defines a modified version of the
-Ada 2005 container for hashed sets, meant to facilitate formal
-verification of code using such containers. The specification of this
-unit is compatible with SPARK 2014.
-
-Note that although this container was designed with formal verification
-in mind, it may well be generally useful in that it is a simplified more
-efficient version than the one defined in the standard. In particular it
-does not have the complex overhead required to detect cursor tampering.
-
-.. _`Ada.Containers.Formal_Ordered_Maps_(a-cforma.ads)`:
-
-``Ada.Containers.Formal_Ordered_Maps`` (:file:`a-cforma.ads`)
-=============================================================
-
-.. index:: Ada.Containers.Formal_Ordered_Maps (a-cforma.ads)
-
-.. index:: Formal container for ordered maps
-
-This child of ``Ada.Containers`` defines a modified version of the
-Ada 2005 container for ordered maps, meant to facilitate formal
-verification of code using such containers. The specification of this
-unit is compatible with SPARK 2014.
-
-Note that although this container was designed with formal verification
-in mind, it may well be generally useful in that it is a simplified more
-efficient version than the one defined in the standard. In particular it
-does not have the complex overhead required to detect cursor tampering.
-
-.. _`Ada.Containers.Formal_Ordered_Sets_(a-cforse.ads)`:
-
-``Ada.Containers.Formal_Ordered_Sets`` (:file:`a-cforse.ads`)
-=============================================================
-
-.. index:: Ada.Containers.Formal_Ordered_Sets (a-cforse.ads)
-
-.. index:: Formal container for ordered sets
-
-This child of ``Ada.Containers`` defines a modified version of the
-Ada 2005 container for ordered sets, meant to facilitate formal
-verification of code using such containers. The specification of this
-unit is compatible with SPARK 2014.
-
-Note that although this container was designed with formal verification
-in mind, it may well be generally useful in that it is a simplified more
-efficient version than the one defined in the standard. In particular it
-does not have the complex overhead required to detect cursor tampering.
-
-.. _`Ada.Containers.Formal_Vectors_(a-cofove.ads)`:
-
-``Ada.Containers.Formal_Vectors`` (:file:`a-cofove.ads`)
-========================================================
-
-.. index:: Ada.Containers.Formal_Vectors (a-cofove.ads)
-
-.. index:: Formal container for vectors
-
-This child of ``Ada.Containers`` defines a modified version of the
-Ada 2005 container for vectors, meant to facilitate formal
-verification of code using such containers. The specification of this
-unit is compatible with SPARK 2014.
-
-Note that although this container was designed with formal verification
-in mind, it may well be generally useful in that it is a simplified more
-efficient version than the one defined in the standard. In particular it
-does not have the complex overhead required to detect cursor tampering.
-
-.. _`Ada.Containers.Formal_Indefinite_Vectors_(a-cfinve.ads)`:
-
-``Ada.Containers.Formal_Indefinite_Vectors`` (:file:`a-cfinve.ads`)
-===================================================================
-
-.. index:: Ada.Containers.Formal_Indefinite_Vectors (a-cfinve.ads)
-
-.. index:: Formal container for vectors
-
-This child of ``Ada.Containers`` defines a modified version of the
-Ada 2005 container for vectors of indefinite elements, meant to
-facilitate formal verification of code using such containers. The
-specification of this unit is compatible with SPARK 2014.
-
-Note that although this container was designed with formal verification
-in mind, it may well be generally useful in that it is a simplified more
-efficient version than the one defined in the standard. In particular it
-does not have the complex overhead required to detect cursor tampering.
-
-.. _`Ada.Containers.Functional_Infinite_Sequences_(a-cfinse.ads)`:
-
-``Ada.Containers.Functional_Infinite_Sequences`` (:file:`a-cfinse.ads`)
-=======================================================================
-
-.. index:: Ada.Containers.Functional_Infinite_Sequences (a-cfinse.ads)
-
-.. index:: Functional Infinite Sequences
-
-This child of ``Ada.Containers`` defines immutable sequences indexed by
-``Big_Integer``. These containers are unbounded and may contain indefinite
-elements. Their API features functions creating new containers from existing
-ones. To remain reasonably efficient, their implementation involves sharing
-between data-structures. As they are functional, that is, no primitives are
-provided which would allow modifying an existing container, these containers
-can still be used safely.
-
-These containers are controlled so that the allocated memory can be reclaimed
-when the container is no longer referenced. Thus, they cannot directly be used
-in contexts where controlled types are not supported.
-The specification of this unit is compatible with SPARK 2014.
-
-.. _`Ada.Containers.Functional_Vectors_(a-cofuve.ads)`:
-
-``Ada.Containers.Functional_Vectors`` (:file:`a-cofuve.ads`)
-============================================================
-
-.. index:: Ada.Containers.Functional_Vectors (a-cofuve.ads)
-
-.. index:: Functional vectors
-
-This child of ``Ada.Containers`` defines immutable vectors. These
-containers are unbounded and may contain indefinite elements. Furthermore, to
-be usable in every context, they are neither controlled nor limited. As they
-are functional, that is, no primitives are provided which would allow modifying
-an existing container, these containers can still be used safely.
-
-Their API features functions creating new containers from existing ones.
-As a consequence, these containers are highly inefficient. They are also
-memory consuming, as the allocated memory is not reclaimed when the container
-is no longer referenced. Thus, they should in general be used in ghost code
-and annotations, so that they can be removed from the final executable. The
-specification of this unit is compatible with SPARK 2014.
-
-.. _`Ada.Containers.Functional_Sets_(a-cofuse.ads)`:
-
-``Ada.Containers.Functional_Sets`` (:file:`a-cofuse.ads`)
-=========================================================
-
-.. index:: Ada.Containers.Functional_Sets (a-cofuse.ads)
-
-.. index:: Functional sets
-
-This child of ``Ada.Containers`` defines immutable sets. These containers are
-unbounded and may contain indefinite elements. Their API features functions
-creating new containers from existing ones. To remain reasonably efficient,
-their implementation involves sharing between data-structures. As they are
-functional, that is, no primitives are provided which would allow modifying an
-existing container, these containers can still be used safely.
-
-These containers are controlled so that the allocated memory can be reclaimed
-when the container is no longer referenced. Thus, they cannot directly be used
-in contexts where controlled types are not supported.
-The specification of this unit is compatible with SPARK 2014.
-
-.. _`Ada.Containers.Functional_Maps_(a-cofuma.ads)`:
-
-``Ada.Containers.Functional_Maps`` (:file:`a-cofuma.ads`)
-=========================================================
-
-.. index:: Ada.Containers.Functional_Maps (a-cofuma.ads)
-
-.. index:: Functional maps
-
-This child of ``Ada.Containers`` defines immutable maps. These containers are
-unbounded and may contain indefinite elements. Their API features functions
-creating new containers from existing ones. To remain reasonably efficient,
-their implementation involves sharing between data-structures. As they are
-functional, that is, no primitives are provided which would allow modifying an
-existing container, these containers can still be used safely.
-
-These containers are controlled so that the allocated memory can be reclaimed
-when the container is no longer referenced. Thus, they cannot directly be used
-in contexts where controlled types are not supported.
-The specification of this unit is compatible with SPARK 2014.
-
 .. _`Ada.Containers.Bounded_Holders_(a-coboho.ads)`:
 
 ``Ada.Containers.Bounded_Holders`` (:file:`a-coboho.ads`)