Vincent Laporte edited this page Feb 26, 2018 · 1 revision


This Coq Working Group took place on December 18th and 19th at Inria Paris (2, rue Simone Iff). Videos are available on Coq's YouTube channel



  • 10h-11h:

  • 11h15-12h15:

    • Attributes (Vincent, 30 min)
    • Integers and arrays (Maxime, 30 min)
  • 14h-15h:

    • API - Emilio
  • 15h30-..: Technical work in groups, subject proposals (need one lead per group, not two groups with same lead).

    • EConstr API completion (taking input from e.g. Equations, ssreflect) Lead: Matthieu Participants: Cyprien? Pierre-Marie? Emilio
    • Evar_source/evar_kinds Lead: ? Participants: Matthieu, ...
    • Future goals and the shelf etc... looking at what unifall-infra adds there. Lead: ? Participants: Maxime, Emilio
    • Porting the ssr plugin to modern APIs Lead: Maxime Participants: Georges ? Pierre-Marie ? Enrico ? Emilio


  • 10h-11h00:

    • Plugin Developer Program (Emilio, 30 min)
    • Fire drill
  • 11h15-12h15:

    • A presentation of TLC 2.0 (covering library design, not tactics) (Arthur, 45min + questions)
  • 14h-15h:

    • Evaluation inside Coq with non-constructive recursive definitions (Arthur, 20 min)
    • Coq Meetup [Théo, Emilio] (15 min)
  • 15h

    • coq-community, a new birth for Coq contribs (Théo, 25 minutes), or Ltac2 (or Ltac3) by Pierre-Marie (or Enrico)
  • 15h30-..: Working groups

PRs that need to be discussed (possibly around a computer)

From oldest to most recent:

Issues that need to be discussed (possibly around a computer)


  • Yves Bertot
  • Cyril Cohen
  • Maxime Dénès
  • Emilio Gallego
  • Gaëtan Gilbert
  • Georges Gonthier
  • Hugo Herbelin
  • Vincent Laporte
  • Guillaume Melquiond
  • Pierre-Marie Pédrot
  • Matthieu Sozeau
  • Enrico Tassi
  • Théo Zimmermann
  • Arthur Charguéraud
  • Cyprien Mangin
Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.