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

1 files changed, 9 insertions, 1 deletions

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 093f1f0b68..a21137a05c 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) ()