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 /library/globnames.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 'library/globnames.ml')
| -rw-r--r-- | library/globnames.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/globnames.ml b/library/globnames.ml index 9d7ab2db8..a6e75fdb6 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -30,7 +30,7 @@ let eq_gr gr1 gr2 = | IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2 | ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2 | VarRef v1, VarRef v2 -> Id.equal v1 v2 - | _ -> false + | (ConstRef _ | IndRef _ | ConstructRef _ | VarRef _), _ -> false let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef" let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef" |