fsetdec : non-atomic elements are now transformed as variables first (fix #2464)

 Btw, we also get rid of equalities on something else than elements or sets

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14525 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 39 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/2464.v b/test-suite/bugs/closed/shouldsucceed/2464.v
new file mode 100644
index 0000000000..af70858720
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2464.v
@@ -0,0 +1,39 @@
+Require Import FSetWeakList.
+Require Import FSetDecide.
+
+Parameter Name : Set.
+Axiom eq_Name_dec : forall (n : Name) (o : Name), {n = o} + {n <> o}.
+
+Module DecidableName.
+Definition t := Name.
+Definition eq := @eq Name.
+Definition eq_refl := @refl_equal Name.
+Definition eq_sym := @sym_eq Name.
+Definition eq_trans := @trans_eq Name.
+Definition eq_dec := eq_Name_dec.
+End DecidableName.
+
+Module NameSetMod := Make(DecidableName).
+
+Module NameSetDec := WDecide (NameSetMod).
+
+Class PartPatchUniverse (pu_type1 pu_type2 : Type)
+                       : Type := mkPartPatchUniverse {
+}.
+Class PatchUniverse {pu_type : Type}
+                    (ppu : PartPatchUniverse pu_type pu_type)
+                  : Type := mkPatchUniverse {
+    pu_nameOf : pu_type -> Name
+}.
+
+Lemma foo : forall (pu_type : Type)
+                   (ppu : PartPatchUniverse pu_type pu_type)
+                   (patchUniverse : PatchUniverse ppu)
+                   (ns ns1 ns2 : NameSetMod.t)
+                   (containsOK : NameSetMod.Equal ns1 ns2)
+                   (p : pu_type)
+                   (HX1 : NameSetMod.Equal ns1 (NameSetMod.add (pu_nameOf p) ns)),
+            NameSetMod.Equal ns2 (NameSetMod.add (pu_nameOf p) ns).
+Proof.
+NameSetDec.fsetdec.
+Qed.
\ No newline at end of file