root edited this page Oct 11, 2017 · 6 revisions


This WG took place September 5th at PPS/Sophie Germain, 3rd floor, in the morning, from 10.30am to 13:30am, then, on an a less formal way during the afternoon.


Pierre Boutillier, Hugo Herbelin, Pierre-Marie Pédrot, Matthieu Sozeau, Bas Spitters, Arnaud Spiwack.

Polymorphic universes

  • Parsing issues: decision to parse <Type@%7Bu>} only when u is a reference to a universe; no parsing for things like <Type@%7BTop.17%7D>.
  • Decision to wait for support from Benjamin Grégoire for supporting vm_compute on polymorphic definitions and from Maxime Dénès for supporting native_compute.
  • checker still to adapt


Matthieu is going to introduce a primitive notion of types with projections for elimination, distinct from the inductive types based on pattern-matching. Decision to compile "match t as x with C y1..yn => t end" into "let x := t in let y1 := proj1 x in ... let yn := projn x in t"

Tactics and new proof engine

The idea of providing a module Tactics.V82 which contains the 8.4 tactics.mli is discussed and seems to be the preferred one for leaving time to users for porting their tactics to the new engine.

Windows and MacOS packages

Pierre Boutillier and Enrico Tassi converge on a similar procedure to release packages on Windows and MacOS, with eventually an ocaml compiler for building compatible plugins.

Naming and parsing existential variables

Hugo proposed a patch for naming evars by name, for printing instance and for being able to reparse evars with instances. Discussed syntax is "?id@[x:=t;y:=u]".

Discussions on giving the possibility of naming evars in refine and co is discussed. Possible notation is ?[id] to mean this is a hole to be named id.

simpl vs cbn

Decision to expect the new cbn to replace simpl (with a flag to restore the old behavior of the name "simpl"). Tentative syntax will be "simpl delta_flag contextually_flag" with "delta_flag" being [cst1 ... cstn] or -[cst1 ... cstn] and contextually_flag being "cst" or "cst at occs".


  • Discussion on having local definitions in evars instances or not? The historical motivation for that was: Consider the unification problem x':T, y':=phi(x'):U |- ?n[x:=x',y:=y'] == psi(y',x') where x:T, y:=phi(x):U |- ?n : V. Thanks to let-in in the instance, it is easy to invert the substitution and infer ?n = psi(y,x) rather than psi(y,phi(x')).
  • Discussion on the semantics of the new Undo and Back in the state transition machine which. They are now document-level commands, i.e. saved as commands. However their semantics changed since they both undo the last command while before Undo was undoing the last tactic invocation and Back the last command. In particular, "Undo" after "Undo" undoes the effect of the first "Undo".
  • Decision to unify the order of env and sigma in OCaml code: env first, then sigma.
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.