The Coq mailing list

[Christopher Ernest Sally <christopherernestsally AT gmail.com>]

Hi Club

In a Module A  in Section a. I have a lemma, R_compat that registers one of my relations as a setoid (roughly speaking) allowing me to rewrite with my defined relation. Further, R_compat takes in a implicit variable from Section a.

Now in Module B, Section b, I have a Variable, var.
I would like to have (@R_compat var) available to every lemma I want to prove in Module B Section b.

I've tried the Hint system, but nothing seems to be working out, on account of it not solving my goals, but instead just allowing me to rewrite.

"Hypothesis" is not good for my situation in this case as I don't want to pass that argument around, since I've already proved R_compat.

Thank you.

Warm regards
Chris