Coq Call 2020 11 18

• November 18th 2020, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• Taking position about #13100, #13102, #13103, ... i.e. on systematically keeping location on parsed identifiers, and propagating this information up towards the error messages when "relevant"
• PR #11390 (implicit arguments in Context): is there some hope to preserve compatibility?
• CEP #49 and PR #11099 (instantiation of non-dependent implicit arguments by name or index): adopting the with model? generalizing it to all (including @foo-style) applied references?

Notes

• Keeping locations on idents for Ltac error messages.

  After discussion with @herbelin and @ppedrot, came to a design where the runtime of Ltac is not impacted but locations can be given to tactics optionally for the interactive mode.

• 11390: we should really evaluate if fixing the contribs is hard, because that's a bugfix and maintaining backward compatibility is going to be hard. We are allowed to break here. Discussion about Variables and Context came back: time to reevaluation if we can merge them. No parsing issue seems unsourmountable.