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/pretyping.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/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b930c5db8..33dd1344f 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -738,6 +738,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre 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 lvar c in + judge_of_projection env.ExtraEnv.env !evdref p cj + | GApp (f,args) -> let fj = pretype empty_tycon env evdref lvar f in let floc = loc_of_glob_constr f in |