From de988641848ecb26f749fbc3f50ce9194db46a4c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 24 Jan 2018 16:45:46 +0100
Subject: Use r.(p) syntax to print primitive projections.

There is no way today to distinguish primitive projections from
compatibility constants, at least in the case of a record without
parameters.

We remedy to this by always using the r.(p) syntax when printing
primitive projections, even with Set Printing All.

The input syntax r.(p) is still elaborated to GApp, so that we can preserve
the compatibility layer. Hopefully we can make up a plan to get rid of that
layer, but it will require fixing a few problems.
---
 intf/constrexpr.ml    | 1 +
 intf/glob_term.ml     | 1 +
 intf/notation_term.ml | 1 +
 intf/pattern.ml       | 2 +-
 4 files changed, 4 insertions(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index 8bcdbcc0ef..fbf9e248ab 100644
--- a/intf/constrexpr.ml
+++ b/intf/constrexpr.ml
@@ -97,6 +97,7 @@ and constr_expr_r =
   | CGeneralization of binding_kind * abstraction_kind option * constr_expr
   | CPrim of prim_token
   | CDelimiters of string * constr_expr
+  | CProj of reference * constr_expr
 and constr_expr = constr_expr_r CAst.t
 
 and case_expr = constr_expr                 (* expression that is being matched *)
diff --git a/intf/glob_term.ml b/intf/glob_term.ml
index f311d33b8a..61bbe2c264 100644
--- a/intf/glob_term.ml
+++ b/intf/glob_term.ml
@@ -55,6 +55,7 @@ type 'a glob_constr_r =
   | GSort of glob_sort
   | GHole of Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option
   | GCast of 'a glob_constr_g * 'a glob_constr_g cast_type
+  | GProj of Projection.t * 'a glob_constr_g
 and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t
 
 and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g
diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index 7823d3febb..cad6f4b821 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -43,6 +43,7 @@ type notation_constr =
       notation_constr array * notation_constr array
   | NSort of glob_sort
   | NCast of notation_constr * notation_constr cast_type
+  | NProj of Projection.t * notation_constr
 
 (** Note concerning NList: first constr is iterator, second is terminator;
     first id is where each argument of the list has to be substituted
diff --git a/intf/pattern.ml b/intf/pattern.ml
index 20636accfa..64873a0394 100644
--- a/intf/pattern.ml
+++ b/intf/pattern.ml
@@ -26,7 +26,7 @@ type constr_pattern =
   | PRel of int
   | PApp of constr_pattern * constr_pattern array
   | PSoApp of patvar * constr_pattern list
-  | PProj of projection * constr_pattern
+  | PProj of Projection.t * constr_pattern
   | PLambda of Name.t * constr_pattern * constr_pattern
   | PProd of Name.t * constr_pattern * constr_pattern
   | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern
-- 
cgit v1.2.3