search

JasonGross / coq-tools

Some scripts to help construct small reproducing examples of bugs, implement [Proof using], etc.
MIT License
38 stars 9 forks source link

Consider preferring `Require Import Coq.Init.Ltac.` over `Declare ML Module "ltac_plugin".`. #107

Closed JasonGross closed 7 months ago

JasonGross commented 2 years ago

@_Théo Zimmermann|299351 said:

This one also doesn't have any comment: https://github.com/coq/coq/pull/14671#issuecomment-881982360

Oh, this one is interesting. It fails to find the error message in the log because the build says transitivity where the new file says Ltac.transitivity, probably because we do Declare ML Module "ltac_plugin". at the top and this shadows transitivity. I guess I should switch to preferring Require Import Coq.Init.Ltac.?

JasonGross commented 7 months ago

Fixed by dda3ece2f89b89f6cd40cb2643b34250427c17ff