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.
---
 pretyping/patternops.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'pretyping/patternops.ml')

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 41e09004c6..1bec4a6f15 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -137,8 +137,7 @@ let rec head_pattern_bound t =
     | PCase (_,p,c,br) -> head_pattern_bound c
     | PRef r         -> r
     | PVar id        -> VarRef id
-    | PProj (p,c)    -> ConstRef (Projection.constant p)
-    | PEvar _ | PRel _ | PMeta _ | PSoApp _  | PSort _ | PFix _
+    | PEvar _ | PRel _ | PMeta _ | PSoApp _  | PSort _ | PFix _ | PProj _
 	-> raise BoundPattern
     (* Perhaps they were arguments, but we don't beta-reduce *)
     | PLambda _ -> raise BoundPattern
@@ -446,6 +445,9 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
 	 one non-trivial branch. These facts are used in [Constrextern]. *)
       PCase (info, pred, pat_of_raw metas vars c, brs)
 
+  | GProj(p,c) ->
+    PProj(p, pat_of_raw metas vars c)
+
   | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GRec _ ->
       err ?loc (Pp.str "Non supported pattern."))
 
-- 
cgit v1.2.3