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.

19 files changed, 81 insertions, 17 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 *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 1330b3741..4f7d537d3 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 61b33aa41..8e99435db 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 20492e38c..326d05cba 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
 
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index 8bcdbcc0e..fbf9e248a 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 f311d33b8..61bbe2c26 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 7823d3feb..cad6f4b82 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 20636accf..64873a039 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
diff --git a/library/globnames.ml b/library/globnames.ml
index 9d7ab2db8..a6e75fdb6 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -30,7 +30,7 @@ let eq_gr gr1 gr2 =
     | IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2
     | ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2
     | VarRef v1, VarRef v2 -> Id.equal v1 v2
-    | _ -> false
+    | (ConstRef _ | IndRef _ | ConstructRef _ | VarRef _), _ -> false
 
 let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef"
 let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef"
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 0b929b8ca..f7639d22d 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -591,6 +591,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 		*)
 		build_entry_lc env funnames avoid (mkGApp(b,args))
 	    | GRec _ -> user_err Pp.(str "Not handled GRec")
+            | GProj _ -> user_err Pp.(str "Funind does not support primitive projections")
 	    | GProd _ -> user_err Pp.(str "Cannot apply a type")
 	end (* end of the application treatement *)
 
@@ -697,6 +698,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
     | GRec _ -> user_err Pp.(str "Not handled GRec")
     | GCast(b,_) ->
 	build_entry_lc env funnames  avoid b
+    | GProj(_,_) -> user_err Pp.(str "Funind does not support primitive projections")
 and build_entry_lc_from_case env funname make_discr
     (el:tomatch_tuples)
     (brl:Glob_term.cases_clauses) avoid :
@@ -1245,7 +1247,7 @@ let rec compute_cst_params relnames params gt = DAst.with_val (function
 		 discrimination ones *)
   | GSort _ -> params
   | GHole _ -> params
-  | GIf _ | GRec _ | GCast _ ->
+  | GIf _ | GRec _ | GCast _ | GProj _ ->
       raise (UserError(Some "compute_cst_params", str "Not handled case"))
   ) gt
 and compute_cst_params_from_app acc (params,rtl) =
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index be8abb92e..b4ca1073c 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -109,6 +109,7 @@ let change_vars =
       | GCast(b,c) ->
 	  GCast(change_vars mapping b,
 		Miscops.map_cast_type (change_vars mapping) c)
+      | GProj(p,c) -> GProj(p, change_vars mapping c)
       ) rt
   and change_vars_br mapping ((loc,(idl,patl,res)) as br) =
     let new_mapping = List.fold_right Id.Map.remove idl mapping in
@@ -293,6 +294,7 @@ let rec alpha_rt excluded rt =
 	GApp(alpha_rt excluded f,
 	     List.map (alpha_rt excluded) args
 	    )
+    | GProj(p,c) -> GProj(p, alpha_rt excluded c)
   in
   new_rt
 
@@ -344,6 +346,7 @@ let is_free_in id =
     | GHole _ -> false
     | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
     | GCast (b,CastCoerce) -> is_free_in b
+    | GProj (_,c) -> is_free_in c
     ) x
   and is_free_in_br (_,(ids,_,rt)) =
     (not (Id.List.mem id ids)) && is_free_in rt
@@ -437,6 +440,8 @@ let replace_var_by_term x_id term =
       | GCast(b,c) ->
 	  GCast(replace_var_by_pattern b,
 		Miscops.map_cast_type replace_var_by_pattern c)
+      | GProj(p,c) ->
+        GProj(p,replace_var_by_pattern c)
     ) x
   and replace_var_by_pattern_br ((loc,(idl,patl,res)) as br) =
     if List.exists (fun id -> Id.compare id x_id == 0) idl
@@ -540,6 +545,7 @@ let expand_as =
       | GCases(sty,po,el,brl) ->
 	  GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
 		List.map (expand_as_br map) brl)
+      | GProj(p,c) -> GProj(p, expand_as map c)
     )
   and expand_as_br map (loc,(idl,cpl,rt)) =
     (loc,(idl,cpl, expand_as (List.fold_left add_as map cpl) rt))
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 071bab2f3..58154d310 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -215,6 +215,7 @@ let is_rec names =
     | GCases(_,_,el,brl) ->
 	List.exists (fun (e,_) -> lookup names e) el ||
 	  List.exists (lookup_br names) brl
+    | GProj(_,c) -> lookup names c
   and lookup_br names (_,(idl,_,rt)) =
     let new_names = List.fold_right Id.Set.remove idl names in
     lookup new_names rt
@@ -779,6 +780,7 @@ let rec add_args id new_args = CAst.map (function
   | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.")
   | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.")
   | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.")
+  | CProj _ -> user_err Pp.(str "Funind does not support primitive projections")
   )
 exception Stop of  Constrexpr.constr_expr
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 23993243f..754e88139 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -581,12 +581,7 @@ and detype_r d flags avoid env sigma t =
     | Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u)
     | Proj (p,c) ->
       let noparams () = 
-	let pb = Environ.lookup_projection p (snd env) in
-	let pars = pb.Declarations.proj_npars in
-	let hole = DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in
-	let args = List.make pars hole in
- 	  GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None),
-		(args @ [detype d flags avoid env sigma c]))
+    GProj (p, detype d flags avoid env sigma c)
       in
       if fst flags || !Flags.in_debugger || !Flags.in_toplevel then
 	try noparams ()
@@ -1002,6 +997,13 @@ let rec subst_glob_constr subst = DAst.map (function
       let r1' = subst_glob_constr subst r1 in
       let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in
       if r1' == r1 && k' == k then raw else GCast (r1',k')
+
+  | GProj (p,c) as raw ->
+    let kn = Projection.constant p in
+    let b = Projection.unfolded p in
+    let kn' = subst_constant subst kn in
+    let c' = subst_glob_constr subst c in
+    if kn' == kn && c' == c then raw else GProj(Projection.make kn' b, c')
   )
 
 (* Utilities to transform kernel cases to simple pattern-matching problem *)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 093f1f0b6..a21137a05 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -133,8 +133,10 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
     Miscops.intro_pattern_naming_eq nam1 nam2
   | GCast (c1, t1), GCast (c2, t2) ->
     f c1 c2 && cast_type_eq f t1 t2
+  | GProj (p1, t1), GProj (p2, t2) ->
+    Projection.equal p1 p2 && f t1 t2
   | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ |
-     GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _), _ -> false
+     GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _ | GProj _), _ -> false
 
 let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c
 
@@ -180,6 +182,8 @@ let map_glob_constr_left_to_right f = DAst.map (function
       let comp1 = f c in
       let comp2 = Miscops.map_cast_type f k in
       GCast (comp1,comp2)
+  | GProj (p,c) ->
+    GProj (p, f c)
   | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) as x -> x
   )
 
@@ -212,6 +216,8 @@ let fold_glob_constr f acc = DAst.with_val (function
     let acc = match k with
       | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in
     f acc c
+  | GProj(_,c) ->
+    f acc c
   | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc
   )
 
@@ -253,6 +259,8 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
     let acc = match k with
       | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in
     f v acc c
+  | GProj(_,c) ->
+    f v acc c
   | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc))
 
 let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 41e09004c..1bec4a6f1 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."))
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b930c5db8..33dd1344f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -738,6 +738,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     let j = pretype_sort ?loc evdref s in
       inh_conv_coerce_to_tycon ?loc env evdref j tycon
 
+  | GProj (p, c) ->
+    (* TODO: once GProj is used as an input syntax, use bidirectional typing here *)
+    let cj = pretype empty_tycon env evdref lvar c in
+    judge_of_projection env.ExtraEnv.env !evdref p cj
+
   | GApp (f,args) ->
     let fj = pretype empty_tycon env evdref lvar f in
     let floc = loc_of_glob_constr f in
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 9f084ae8d..153a48a71 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -53,3 +53,4 @@ val judge_of_abstraction : Environ.env -> Name.t ->
   unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment
 val judge_of_product : Environ.env -> Name.t ->
   unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment
+val judge_of_projection : env -> evar_map -> projection -> unsafe_judgment -> unsafe_judgment
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 51735bc9e..1146b42a0 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -732,6 +732,9 @@ let tag_var = tag Tag.variable
         return (pr_prim_token p, prec_of_prim_token p)
       | CDelimiters (sc,a) ->
         return (pr_delimiters sc (pr mt (ldelim,E) a), ldelim)
+      | CProj (p,c) ->
+        let p = pr_proj (pr mt) pr_app c (CAst.make (CRef (p,None))) [] in
+        return (p, lproj)
     in
     let loc = constr_loc a in
     pr_with_comments ?loc
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index d6d410d1a..668b4e578 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -5,7 +5,7 @@ PWrap has primitive projections with eta conversion.
 For PWrap: Argument scope is [type_scope]
 For pwrap: Argument scopes are [type_scope _]
 punwrap@{u} = 
-fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p
+fun (A : Type@{u}) (p : PWrap@{u} A) => p.(punwrap)
      : forall A : Type@{u}, PWrap@{u} A -> A
 (* u |=  *)