I have a file `F`

that transitively `Require Import`

s another file `G`

, which `Require Import`

s `Equations.Prop`

.

Is it a bug of Coq that in `F`

, the implicit `Arguments`

of `eq_refl`

are not the same before and after `Import`

ing G?

(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 )

who changes `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 `Export Arguments`

.

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: Jun 11 2023 at 00:30 UTC