summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed/1738.v
blob: 0deed3663b668c1785b6c4e6ef713f31df8aed13 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
Require Import FSets.

Module SomeSetoids (Import M:FSetInterface.S).

Lemma Equal_refl : forall s, s[=]s.
Proof. red; split; auto. Qed.

Add Relation t Equal 
 reflexivity proved by Equal_refl 
 symmetry proved by eq_sym
 transitivity proved by eq_trans 
 as EqualSetoid.

Add Morphism Empty with signature Equal ==> iff as Empty_m.
Proof.
unfold Equal, Empty; firstorder.
Qed.

End SomeSetoids.

Module Test (Import M:FSetInterface.S).
 Module A:=SomeSetoids M.
 Module B:=SomeSetoids M. (* lots of warning *)

 Lemma Test : forall s s', s[=]s' -> Empty s -> Empty s'.
 intros.
 rewrite H in H0.
 assumption.
Qed.
End Test.