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

5 files changed, 7 insertions, 24 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 6a9a042f57..0dc5a9bad5 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -675,8 +675,12 @@ and detype_r d flags avoid env sigma t =
         (Array.map_to_list (detype d flags avoid env sigma) args)
     | Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u)
     | Proj (p,c) ->
-      let noparams () = 
-    GProj (p, detype d flags avoid env sigma c)
+      let noparams () =
+        let pars = Projection.npars p in
+        let hole = DAst.make @@ GHole(Evar_kinds.InternalHole,Namegen.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]))
       in
       if fst flags || !Flags.in_debugger || !Flags.in_toplevel then
 	try noparams ()
@@ -1030,10 +1034,6 @@ let rec subst_glob_constr subst = DAst.map (function
       let k' = 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 p' = subst_proj subst p in
-    let c' = subst_glob_constr subst c in
-    if p' == p && c' == c then raw else GProj(p', c')
   )
 
 (* Utilities to transform kernel cases to simple pattern-matching problem *)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index bd13f1d00a..9b2da0b084 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -152,10 +152,8 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
     Namegen.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 _ | GProj _), _ -> false
+     GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _ ), _ -> false
 
 let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c
 
@@ -216,8 +214,6 @@ let map_glob_constr_left_to_right f = DAst.map (function
       let comp1 = f c in
       let comp2 = 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
   )
 
@@ -250,8 +246,6 @@ 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
   )
 
@@ -295,8 +289,6 @@ 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/glob_term.ml b/pretyping/glob_term.ml
index 86245d4794..c6fdb0ec14 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -82,7 +82,6 @@ type 'a glob_constr_r =
   | GSort of glob_sort
   | GHole of Evar_kinds.t * Namegen.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/pretyping/patternops.ml b/pretyping/patternops.ml
index f7fea22c0f..3c1c470053 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -464,9 +464,6 @@ 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)
-
   | GRec (GFix (ln,n), ids, decls, tl, cl) ->
     if Array.exists (function (Some n, GStructRec) -> false | _ -> true) ln then
       err ?loc (Pp.str "\"struct\" annotation is expected.")
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 162adf0626..a40c0d2375 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -613,11 +613,6 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref
     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 c in
-    judge_of_projection !!env !evdref p cj
-
   | GApp (f,args) ->
     let fj = pretype empty_tycon env evdref f in
     let floc = loc_of_glob_constr f in