4 files changed, 73 insertions, 20 deletions
diff --git a/doc/sphinx/language/core/primitive.rst b/doc/sphinx/language/core/primitive.rst
index dc8f131209..727177b23a 100644
--- a/doc/sphinx/language/core/primitive.rst
+++ b/doc/sphinx/language/core/primitive.rst
@@ -40,9 +40,8 @@ These primitive declarations are regular axioms. As such, they must be trusted a
 
    Print Assumptions one_minus_one_is_zero.
 
-The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement
-dedicated, efficient, rules to reduce the applications of these primitive
-operations.
+The reduction machines implement dedicated, efficient rules to reduce the
+applications of these primitive operations.
 
 The extraction of these primitives can be customized similarly to the extraction
 of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlInt63`
@@ -105,3 +104,53 @@ Literal values (of type :g:`Float64.t`) are extracted to literal OCaml
 values (of type :g:`float`) written in hexadecimal notation and
 wrapped into the :g:`Float64.of_float` constructor, e.g.:
 :g:`Float64.of_float (0x1p+0)`.
+
+.. _primitive-arrays:
+
+Primitive Arrays
+----------------
+
+The language of terms features persistent arrays as values. The type of
+such a value is *axiomatized*; it is declared through the following sentence
+(excerpt from the :g:`PArray` module):
+
+.. coqdoc::
+
+   Primitive array := #array_type.
+
+This type is equipped with a few operators, that must be similarly declared.
+For instance, elements in an array can be accessed and updated using the
+:g:`PArray.get` and :g:`PArray.set` functions, declared and specified as
+follows:
+
+.. coqdoc::
+
+   Primitive get := #array_get.
+   Primitive set := #array_set.
+   Notation "t .[ i ]" := (get t i).
+   Notation "t .[ i <- a ]" := (set t i a).
+
+   Axiom get_set_same : forall A t i (a:A), (i < length t) = true -> t.[i<-a].[i] = a.
+   Axiom get_set_other : forall A t i j (a:A), i <> j -> t.[i<-a].[j] = t.[j].
+
+The complete set of such operators can be obtained looking at the :g:`PArray` module.
+
+These primitive declarations are regular axioms. As such, they must be trusted and are listed by the
+:g:`Print Assumptions` command.
+
+The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement
+dedicated, efficient rules to reduce the applications of these primitive
+operations.
+
+The extraction of these primitives can be customized similarly to the extraction
+of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlPArray`
+module can be used when extracting to OCaml: it maps the Coq primitives to types
+and functions of a :g:`Parray` module. Said OCaml module is not produced by
+extraction. Instead, it has to be provided by the user (if they want to compile
+or execute the extracted code). For instance, an implementation of this module
+can be taken from the kernel of Coq (see ``kernel/parray.ml``).
+
+Primitive arrays expose a functional interface, but they are internally
+implemented using a persistent data structure :cite:`ConchonFilliatre07wml`.
+Update and access to an element in the most recent copy of an array are
+constant time operations.
diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst
index 40e0898871..20f4310d13 100644
--- a/doc/sphinx/language/extensions/evars.rst
+++ b/doc/sphinx/language/extensions/evars.rst
@@ -13,13 +13,13 @@ Existential variables
    | ?[ ?@ident ]
    | ?@ident {? @%{ {+; @ident := @term } %} }
 
-|Coq| terms can include existential variables which represents unknown
-subterms to eventually be replaced by actual subterms.
+|Coq| terms can include existential variables that represent unknown
+subterms that are eventually replaced with actual subterms.
 
-Existential variables are generated in place of unsolvable implicit
+Existential variables are generated in place of unsolved implicit
 arguments or “_” placeholders when using commands such as ``Check`` (see
 Section :ref:`requests-to-the-environment`) or when using tactics such as
-:tacn:`refine`, as well as in place of unsolvable instances when using
+:tacn:`refine`, as well as in place of unsolved instances when using
 tactics such that :tacn:`eapply`. An existential
 variable is defined in a context, which is the context of variables of
 the placeholder which generated the existential variable, and a type,
@@ -43,22 +43,18 @@ existential variable is represented by “?” followed by an identifier.
    Check identity _ (fun x => _).
 
 In the general case, when an existential variable :n:`?@ident` appears
-outside of its context of definition, its instance, written under the
-form :n:`{ {*; @ident := @term} }` is appending to its name, indicating
+outside its context of definition, its instance, written in the
+form :n:`{ {*; @ident := @term} }`, is appended to its name, indicating
 how the variables of its defining context are instantiated.
-The variables of the context of the existential variables which are
-instantiated by themselves are not written, unless the :flag:`Printing Existential Instances` flag
-is on (see Section :ref:`explicit-display-existentials`), and this is why an
-existential variable used in the same context as its context of definition is written with no instance.
+Only the variables that are defined in another context are displayed:
+this is why an existential variable used in the same context as its
+context of definition is written with no instance.
+This behaviour may be changed: see :ref:`explicit-display-existentials`.
 
 .. coqtop:: all
 
    Check (fun x y => _) 0 1.
 
-   Set Printing Existential Instances.
-
-   Check (fun x y => _) 0 1.
-
 Existential variables can be named by the user upon creation using
 the syntax :n:`?[@ident]`. This is useful when the existential
 variable needs to be explicitly handled later in the script (e.g.
@@ -88,6 +84,14 @@ Explicit displaying of existential instances for pretty-printing
    context of an existential variable is instantiated at each of the
    occurrences of the existential variable.
 
+.. coqtop:: all
+
+   Check (fun x y => _) 0 1.
+
+   Set Printing Existential Instances.
+
+   Check (fun x y => _) 0 1.
+
 .. _tactics-in-terms:
 
 Solving existential variables using tactics
diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst
index bbd486e3ba..ca69072cb9 100644
--- a/doc/sphinx/language/extensions/implicit-arguments.rst
+++ b/doc/sphinx/language/extensions/implicit-arguments.rst
@@ -70,7 +70,7 @@ is said *contextual* if it can be inferred only from the knowledge of
 the type of the context of the current expression. For instance, the
 only argument of::
 
-  nil : forall A:Set, list A`
+  nil : forall A:Set, list A
 
 is contextual. Similarly, both arguments of a term of type::
 
@@ -539,7 +539,7 @@ with free variables into a closed statement where these variables are
 quantified explicitly.  Use the :cmd:`Generalizable` command to designate
 which variables should be generalized.
 
-It is activated for a binder by prefixing a \`, and for terms by
+It is activated within a binder by prefixing it with \`, and for terms by
 surrounding it with \`{ }, or \`[ ] or \`( ).
 
 Terms surrounded by \`{ } introduce their free variables as maximally
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index b4558ef07f..d6a828521f 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -94,7 +94,7 @@ The expression :n:`let ( {*, @ident__i } ) := @term__0 in @term__1`
 performs case analysis on :n:`@term__0` whose type must be an
 inductive type with exactly one constructor.  The number of variables
 :n:`@ident__i` must correspond to the number of arguments of this
-contrustor.  Then, in :n:`@term__1`, these variables are bound to the
+constructor.  Then, in :n:`@term__1`, these variables are bound to the
 arguments of the constructor in :n:`@term__0`.  For instance, the
 definition