diff --git a/gcc/ada/doc/gnat_rm/the_gnat_library.rst b/gcc/ada/doc/gnat_rm/the_gnat_library.rst --- a/gcc/ada/doc/gnat_rm/the_gnat_library.rst +++ b/gcc/ada/doc/gnat_rm/the_gnat_library.rst @@ -285,17 +285,16 @@ specification of this unit is compatible with SPARK 2014. .. index:: Functional sets This child of ``Ada.Containers`` defines immutable sets. 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. +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. -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. +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)`: @@ -307,17 +306,16 @@ specification of this unit is compatible with SPARK 2014. .. index:: Functional maps This child of ``Ada.Containers`` defines immutable maps. 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. +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)`: diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -23520,17 +23520,16 @@ specification of this unit is compatible with SPARK 2014. @geindex Functional sets This child of @code{Ada.Containers} defines immutable sets. 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. +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. -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. +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. @node Ada Containers Functional_Maps a-cofuma ads,Ada Containers Bounded_Holders a-coboho ads,Ada Containers Functional_Sets a-cofuse ads,The GNAT Library @anchor{gnat_rm/the_gnat_library ada-containers-functional-maps-a-cofuma-ads}@anchor{2f4}@anchor{gnat_rm/the_gnat_library id16}@anchor{2f5} @@ -23542,17 +23541,16 @@ specification of this unit is compatible with SPARK 2014. @geindex Functional maps This child of @code{Ada.Containers} defines immutable maps. 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. +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. @node Ada Containers Bounded_Holders a-coboho ads,Ada Command_Line Environment a-colien ads,Ada Containers Functional_Maps a-cofuma ads,The GNAT Library @anchor{gnat_rm/the_gnat_library ada-containers-bounded-holders-a-coboho-ads}@anchor{2f6}@anchor{gnat_rm/the_gnat_library id17}@anchor{2f7}