Merge PR #9391: Clarify meaning of Primitive Projections

Reviewed-by: Zimmi48

1 files changed, 2 insertions, 1 deletions

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index d0e44cd212..50a56f1d51 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