The Coq mailing list

[Johannes Kloos <jkloos AT unix-ag.uni-kl.de>]

On Sun, Aug 10, 2014 at 01:28:39AM +0800, Christopher Ernest Sally wrote:
> 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.

Would this work?

Instance: Setoid var := @R_compat var.

> Thank you.
> 
> Warm regards
> Chris