The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

The anomaly is definitely not intended, please report it as a bug on the issue tracker.  I suspect the other behavior is somewhere between intended and accidental.

On Wed, Dec 2, 2020, 22:33 jonikelee AT gmail.com <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?:

Module Type Foo.
  Ltac tac := idtac "you didn't instantiate Foo.tac!".
End Foo.

Module Bar(Export F:Foo).
  Ltac dobar := tac.
  Goal True.
    dobar. (*Prints "you didn't instantiate Foo.tac!"*)
  Abort.
End Bar.

Module Baz <: Foo.
  Ltac tac := idtac "Baz.tac called!".
End Baz.

Module Beep <: Foo.
  Ltac tac := idtac "Beep.tac called!".
End Beep.

Module Burp <: Foo.
  (*No tac defined here*)
End Burp. (*Not an error, unlike with missing Parameters*)

Module Test.
  Module BarBaz := Bar Baz.
  Module BarBeep := Bar Beep.
  Module BarBurp := Bar Burp.

  Goal True.
    BarBaz.dobar. (*Prints "Baz.tac called!"*)
    BarBeep.dobar. (*Prints "Beep.tac called!"*)
    Fail BarBurp.dobar. (*Oops! - an Anomaly "Uncaught exception Not_Found."*)
  Abort.
End Test.

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?