Adapt to coq/coq#8829 (Error when [foo.(bar)] is used with nonprojection [bar])
Merge request reports
Activity
42 42 Qed. 43 43 44 44 Global Instance uniq_bor_wf κ ty `{!TyWf ty} : TyWf (uniq_bor κ ty) := 45 { ty_lfts := [κ]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) κ }. 45 { ty_lfts := [κ]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty κ }. 
Hm, can't we make some of these records primitive instead?
Have another look, ty_outlives_E is a regular definition, not a record projection. The Coq now errors on regular definitions but still permits emulated projections, with a warning that you're free to disable and which I ignored when making this MR.
-
Oh, I see.
Hm, I have to admit I quite liked being able to use "fake projections", it communicates intent very well IMO. But I suppose you have good reasons for removing that ability.
@jjourdan what do you think?
I think I do agree with @jung that it is nicer to be able to define "fake projections". It gives a taste of "object oriented programming" to Record.
But really, I will not strongly argue for this.
-
Okay. I'll merge this to avoid blocking Coq, but @SkySkimmer please consider this feedback for there being good use-cases for "fake projections".
mentioned in commit 37640c4b
