diff options
Diffstat (limited to 'pretyping/glob_ops.ml')
| -rw-r--r-- | pretyping/glob_ops.ml | 10 |
1 files changed, 1 insertions, 9 deletions
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) () |