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.

4 files changed, 34 insertions, 4 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 7cc8de85d2..da04d8786b 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 *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 1330b3741e..4f7d537d3f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -908,6 +908,9 @@ let rec extern inctx scopes vars r =
   | GCast (c, c') ->
       CCast (sub_extern true scopes vars c,
 	     Miscops.map_cast_type (extern_typ scopes vars) c')
+  | GProj (p, c) ->
+    let pr = extern_reference ?loc Id.Set.empty (ConstRef (Projection.constant p)) in
+    CProj (pr, sub_extern inctx scopes vars c)
   ) r'
 
 and extern_typ (_,scopes) =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 61b33aa415..8e99435dbc 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1869,7 +1869,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     | CCast (c1, c2) ->
 	DAst.make ?loc @@
         GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2)
-  )
+    | CProj (pr, c) ->
+      match intern_reference pr with
+      | ConstRef p ->
+        DAst.make ?loc @@ GProj (Projection.make p false, intern env c)
+      | _ ->
+        raise (InternalizationError (loc,IllegalMetavariable)) (* FIXME *)
+    )
   and intern_type env = intern (set_type_scope env)
 
   and intern_local_binder env bind : intern_env * Glob_term.extended_glob_local_binder list =
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 20492e38c8..326d05cba6 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -86,9 +86,11 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
   Miscops.glob_sort_eq s1 s2
 | NCast (t1, c1), NCast (t2, c2) ->
   (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2
+| NProj (p1, c1), NProj (p2, c2) ->
+  Projection.equal p1 p2 && eq_notation_constr vars c1 c2
 | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
   | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
-  | NRec _ | NSort _ | NCast _), _ -> false
+  | NRec _ | NSort _ | NCast _ | NProj _), _ -> false
 
 (**********************************************************************)
 (* Re-interpret a notation as a glob_constr, taking care of binders   *)
@@ -189,6 +191,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
   | NSort x -> GSort x
   | NHole (x, naming, arg)  -> GHole (x, naming, arg)
   | NRef x -> GRef (x,None)
+  | NProj (p,c) -> GProj (p, f e c)
 
 let glob_constr_of_notation_constr ?loc x =
   let rec aux () x =
@@ -383,6 +386,7 @@ let notation_constr_and_vars_of_glob_constr a =
      if arg != None then has_ltac := true;
      NHole (w, naming, arg)
   | GRef (r,_) -> NRef r
+  | GProj (p, c) -> NProj (p, aux c)
   | GEvar _ | GPatVar _ ->
       user_err Pp.(str "Existential variables not allowed in notations.")
   ) x
@@ -576,6 +580,14 @@ let rec subst_notation_constr subst bound raw =
       let k' = Miscops.smartmap_cast_type (subst_notation_constr subst bound) k in
       if r1' == r1 && k' == k then raw else NCast(r1',k')
 
+  | NProj (p, c) ->
+    let kn = Projection.constant p in
+    let b = Projection.unfolded p in
+    let kn' = subst_constant subst kn in
+    let c' = subst_notation_constr subst bound c in
+    if kn' == kn && c' == c then raw else NProj(Projection.make kn' b, c')
+
+
 let subst_interpretation subst (metas,pat) =
   let bound = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty metas in
   (metas,subst_notation_constr subst bound pat)
@@ -1167,9 +1179,12 @@ let rec match_ inner u alp metas sigma a1 a2 =
           match_names metas (alp,sigma) (Name id') na in
       match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2
 
+  | GProj(p1, t1), NProj(p2, t2) when Projection.equal p1 p2 ->
+    match_in u alp metas sigma t1 t2
+
   | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _
      | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
-     | GCast _), _ -> raise No_match
+     | GCast _ | GProj _ ), _ -> raise No_match
 
 and match_in u = match_ true u