Coq Call 2022 06 01 - rocq-prover/rocq GitHub Wiki

• June 1st, 2022, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• https://github.com/coq/coq/pull/16100 (Emilio, what's going on here?)
• https://github.com/coq/coq/pull/16122 (warning 40)
• can I add a field to https://github.com/coq/coq/blob/4c713ddcf0ebded388b9349938f4371c9c1a254e/kernel/context.ml#L34 to implement let x #[canonical=yes] : S := K v in ...? (it would also allow to fun x #[instance=no] : Class => ...). Morally it is the clean version of encoding this bit of information in the name of the variable (but adds one pointer to binder_annot) (Enrico)