Skip to content

Coq Call 2019 11 20

Emilio Jesus Gallego Arias edited this page Nov 20, 2019 · 11 revisions

November 20th, 4pm Paris Time



  • Fix for template poly ok with Pierre-Marie

  • 8.12 RMs: Emilio and Théo

  • RM for 8.11: hashes for 8.11 versions of libraries in CI: the majority seems to favor that over asking for user branches (esp for .v only libraries that should work with multiple versions).

  • Role of side effects in declare (Emilio)

    • Cleanups coming about side effect handling in declare_def to move to the STM / higher-levels
    • Mainly for defined proofs to clean the handling of side effect export/handling.
  • Implicit Arguments (Hugo)

    • Many questions of design and a few (7) PRs of cleanup.
    • Would be good to have a summary of the changes and use-cases.
      • What are the arguments for keeping non-maximal implicits, if we keep them shall we add [] to terms?
      • Check (c : T) requiring a coercion in front of c, should it print it or not?
      • Same for implicits, what should defensive/not defensive do: is it not rather a UI issue as we can't just have a do-it all Print?
    • Maxime asks what could be a goal design/feature set for implicits in the future.

Joining the call:

Vous êtes invité à la réunion en ligne "Coq Call".

Pour rejoindre :

You're invited to "Coq Call" online meeting.

To join :

Clone this wiki locally
You can’t perform that action at this time.