Merge PR #6651: Use r.(p) syntax to print primitive projections.

5 files changed, 27 insertions, 9 deletions

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 92dab24e2..8809558ff 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -737,6 +737,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