Clarify meaning of Primitive Projections

The previous language makes it seem as if record parameters are automatically set as implicit for the projection functions, but (per discussion with @jasongross) the omission of parameters from primitive projection only takes effect in Coq's internal AST.

1 files changed, 2 insertions, 1 deletions

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 376a6b8eed..f31b64f8a4 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -234,7 +234,8 @@ Primitive Projections
    extended the Calculus of Inductive Constructions with a new binary
    term constructor `r.(p)` representing a primitive projection `p` applied
    to a record object `r` (i.e., primitive projections are always applied).
-   Even if the record type has parameters, these do not appear at
+   Even if the record type has parameters, these do not appear
+   in the internal representation of
    applications of the projection, considerably reducing the sizes of
    terms when manipulating parameterized records and type checking time.
    On the user level, primitive projections can be used as a replacement