diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-01-24 16:45:46 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-30 14:19:57 +0100 |
commit | de988641848ecb26f749fbc3f50ce9194db46a4c (patch) | |
tree | 7eb76c35fb7c4543f91405266d54523026403c54 /pretyping/glob_ops.ml | |
parent | 879ebad4d0b39fda275a72ba44c1f4dfbb9282e5 (diff) |
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.
Diffstat (limited to 'pretyping/glob_ops.ml')
-rw-r--r-- | pretyping/glob_ops.ml | 10 |
1 files changed, 9 insertions, 1 deletions
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) () |