Rodolphe Lepigre

@ejgallego if you could summarize what needs to be done, I can probably help to push this trough soonish. I'm also wondering: do the `.elpi` files need to be installed?...

We now have a more detailed data point on this: we actually got a 10% speedup overall (on our whole Coq development) by removing all imports of MetaCoq, which we...

That was fast, thanks! > * should we warn for variable names starting with `_`? (current code does) I don't care personally, I am fine with also giving a warning...

I found two cases where there should be no warning: - non-linear variables in patterns, - second-order variables in patterns cannot be named `_` (if I remember correctly).

> Can you write an example? There you go: ```coq (* Non-linear pattern variables should not lead to a warning even if unused outside of the pattern. *) Ltac2 useless_hyp_name...

> The easy fix is to disable the warning when the variable name starts with an `_`, so you can write True, I guess I'd be fine with that, and...

> ``` > | [ |- forall x, ?b ] => true (* Here we cannot even replace [?b] by [_]. *) > ``` > > Why not? As far...

This MR seems ready, any reason not to merge it @SkySkimmer? We've been using (the first version of) it for a few months, and it has been really helpful. It...

For the record, we are interested in the new `tclCATCHSYSTEM` primitive introduced by this MR. In our case, we want to catch the `Timeout` exception raised internally by the `Timeout`...

What we are interested in is indeed a kind of `try_finally` function, where the `finally` part would run even when the tactic is interrupted by a timeout or something like...