Rocq Call 2026 09 22 - rocq-prover/rocq GitHub Wiki

Topics

Roles

  • Chairman: Nicolas Tabareau
  • Secretary: Matthieu Sozeau
  • Attending: Matthieu Sozeau, Wassim Ait-Moussa, Theo Zimmermann, Yann Leray, Pierre-Marie Pédrot, Nicolas Tabareau, Guillaume Melquiond, Enrico Tassi

Notes

  • Ltac2 is_section_variable: merge, it is a useful API.
  • lazy profiler: PMP raises issue of adding more code to cClosure.ml. Also this has some performance impact even when off. Decision: ask Janno if it's possible to make it more efficient, and what a compile-time option (a la ppx_optcomp) would do to the code?
  • noopaques: abandon for now.