The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

> On Nov 21, 2014, at 1:13 , Vadim Zaliva 
> <vzaliva AT cmu.edu>
>  wrote:
> 
> Global Instance vconsR_proper `{Equiv A} n:
>  Proper (@vec_equiv A _ n ==> (=) ==> @vec_equiv A _ (S n))
>         (@VConsR A n).

I have also a related question on the scope of instances.

If I put the instantiation above in, say file A.v
and in B.v import it via  "Require Import A" it is not
working. If I move this instantiation to B.v - everything 
works. Why is that?


Sincerely,
Vadim Zaliva

--
CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva