The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 12/04/2016 14:16, Robbert Krebbers wrote:
> Can you give us some idea of the "global picture" that you are after?

Turn Ltac into a mini-ML with backtracking as the built-in effect?

That requires a few things, amongst which:

1. Stick to a proper calling convention (namely CBV)
2. Clearly separate syntax from semantics (mostly already done in trunk)
3. Add datatypes (the semantics is already there, we essentially need a
syntax)

We could probably add

4. Add a typing system

but I'm afraid that this one is too backward-incompatible. Point 1 is
going to break things, while 2 and 3 are mostly backward-compatible.

There are some blocking points regarding compatibility that impede a
real progress, but I am close to being able to provide Ltac as a plugin,
so that one could separate the version of Ltac from the one of Coq, and
dynamically change the version of the language used.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature