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.

1 files changed, 7 insertions, 1 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 7cc8de85d..da04d8786 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -173,10 +173,12 @@ let rec constr_expr_eq e1 e2 =
     | CDelimiters(s1,e1), CDelimiters(s2,e2) ->
       String.equal s1 s2 &&
       constr_expr_eq e1 e2
+    | CProj(p1,c1), CProj(p2,c2) ->
+      eq_reference p1 p2 && constr_expr_eq c1 c2
   | (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _
      | CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _
      | CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _
-     | CGeneralization _ | CDelimiters _), _ -> false
+     | CGeneralization _ | CDelimiters _ | CProj _), _ -> false
 
 and args_eq (a1,e1) (a2,e2) =
   Option.equal (eq_located explicitation_eq) e1 e2 &&
@@ -365,6 +367,8 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
             (fold_local_binders g f n acc t lb) c lb) l acc
     | CCoFix (_,_) ->
       Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc
+    | CProj (_,c) ->
+        f n acc c
   )
 
 let free_vars_of_constr_expr c =
@@ -446,6 +450,8 @@ let map_constr_expr_with_binders g f e = CAst.map (function
           let e'' = List.fold_left (fun e ((_,id),_,_,_) -> g id e) e' dl in
           let d' = f e'' d in
           (id,bl',t',d')) dl)
+    | CProj (p,c) ->
+      CProj (p, f e c)
   )
 
 (* Used in constrintern *)