The Coq mailing list

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

On 03/12/2020 04:33, jonikelee AT gmail.com wrote:
> Did anyone know that it works to define Ltac in a Module Type, such
> that instantiations of that Module Type with an instantiated Ltac def
> (mostly) works?:
> 
> This is in 8.12.  I haven't tried Ltac2 yet - hopefully, the
> instantiations are required to type match the abstration.  Also, I
> think it would be better if End Burp produced an error due to the
> missing tac instantiation, instead of deferring the error (as an
> Anomaly, no less) until runtime.  That is, assuming this is all
> intended behavior, which I hope it is...  Is it?

It's known, and can be considered a feature-ish bug. It's essentially a
variant of the trick described here:

https://github.com/coq/coq/issues/2199

Please don't do that in Ltac2 though, this is a known source of type
unsoundness which is currently not fixable in the current module
architecture. The best we can do is to forbid the definition of Ltac2
types inside a module type, but even there one can probably weasel their
way around using Include.

PMP

Attachment: OpenPGP_signature
Description: OpenPGP digital signature