I have a file
F that transitively
Require Imports another file
Is it a bug of Coq that in
F, the implicit
eq_refl are not the same before and after
(coq 8.12 and equations 1.2.3+8.12)
I rephrase my question: Is this a known bug or should i investige this further and open an issue?
Oh, ok... https://github.com/coq/coq/issues/9902 (EDIT: more likely https://github.com/coq/coq/issues/7654 )
eq_refl’s arguments, G or Equations? I guess your point is that it’s Equations?
(Global) Hint Resolve has similar problems — it propagates on Require, not Import; for Coq 8.12, you can use
Export Hint Resolve and have it propagate only when imported.
I finished my thought in your second issue; you (and they) want
and you’re also asking Equations to migrate to it.
I often end up with one or more
prelude files that imports sets of dependencies and reset any global settings as needed — e.g. I load libraries A and B, which both change
Obligation Tactic, then I set it again — so that everybody importing the prelude gets what the prelude sets, instead of throwing a coin through imports.
Yes, Equation.Prop.Init changes eq_refl's implicit arguments, so it's a problem with equations, right.
Last updated: Jan 29 2023 at 16:02 UTC