Skip to content

Coq Call 2024 05 21

Hugo Herbelin edited this page May 20, 2024 · 9 revisions

Participants:

Topics

  • Looking for feedback on attributes #[sealed] and #[unsealed] (#19029) [Hugo, 10 mins]
    • in particular, adding the ability of attributes per item of a mutual declaration?
  • Looking for feedback on the merge of execution paths for Fixpoint and universes (#18871) [Hugo, 10 mins]
    • in particular, opportunity of splitting the PR into smaller components
  • Looking for feedback on CEP #89 about merging the universe execution paths in declare.ml [Hugo, 20 mins]

Roles

  • Chairman:
  • Secretary:

Notes

Clone this wiki locally