The Coq mailing list

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

On 11/03/2016 21:58, Arnaud Spiwack wrote:
> Of course, for Coq, this is probably unworkable. Pretyping is the most
> sensitive part of Coq and making everything subtly different in
> unpredictable ways is probably not worth the huge effort this would
> represent.

I'm not sure that the pretyper by itself would be difficult to port to
the monad, at least for the pretyping.ml file. This would make it
compatible with the tactic-in-term bactracking. What would be more
difficult would be the unification stuff.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature