Pierre-Marie Pédrot

@herbelin It's not very hard to pass an extra-argument to TACTIC EXTEND with a canonical name, which allows to keep the code working without modifying it. This is already what...

I'm failing to see why we need an extra layer of complexity to implement static binding of versioned tactics. Why not simply piggy back on the module system? We can...

Correction to my above post: we wouldn't shadow parsing rules, but tactic notations. Apart from the last handful of hardwired tactics, every ML tactic now relies on tactic notations to...

@herbelin So, you can't write Ltac86.rewrite because most of ML-side tactics are defined by tactic notations, so this wouldn't even parse. Nonetheless, nowadays most of built-in tactics are defined through...

> So, an Import methodology will not be able alone to deal with configurability. Configurability is a distinct, subtly related matter. I don't think we would gain clarity by confusing...

@herbelin I can provide a POC patch if you want to see what I mean.

Using object is probably a bad idea, but we might use them just for subtyping and phantom types, as done e.g. in js_of_ocaml.

> The name that is stored in the Lam node is a pretty printing hint only, it has not to have any meaning (observable by CIC or Ltac). If only!...

> This is even more fun: the name is there, but the system uses what the pretty printer would print... amazing!!! Yeah, this is actually even a source of slowness...

FTR I have had firstorder on my radar for a while. It's very inefficient because it strongly normalizes all terms from the context. (It's a bit sad that these instances...