From 8d6d5e3107f2b5f075d7daca69eeaf5fbbd7d0f4 Mon Sep 17 00:00:00 2001
From: David A. Dalrymple
Date: Wed, 23 Jan 2019 18:19:28 -0500
Subject: 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.---
 doc/sphinx/language/gallina-extensions.rst | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3