Matthieu Sozeau

We're working on it

Yes, `x`, `y` and. `z` should be `meta.234` etc...

Maybe you can use `Pretty.print_term` to get a nicer output

- I think it is a good convention to keep a license header, maybe referring to the LICENSE file for details. - It's hard to set globally an option without...

I’m not sure I understand why we would need a new toplevel command, shouldn’t the run_template_program in the first example return an Ast.term instead?

I think you need UIP to derive this as you have a non-linear pattern `(tarr t t)` in your index.

That's to be expected indeed. We should indeed have a way to call `vm_compute` and not just `vm_cast`.

Hi, I think I fixed that issue: the principles proof tactics did not have access to the inferred recursive argument of functions. You can try out annotating with “by struct...

In the fix the inferred argument is properly passed to the automation of course

It should be derived properly, maybe you need the fix (branches 8.8 / 8.9 and master all have it now if you follow any of those). Otherwise, maybe having a...