Improved handling of element equalities in fsetdec (fix #2467)

 - We now handle things like (H : E.eq x x -> ...)  by rewriting
   E.eq x x into True.

 - There was also a confusion between E.t and its various equivalent
   (but syntactically different) forms. This should be solved by
   preventing inlining during an inner functor application.

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

2 files changed, 49 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/bug1912.v b/test-suite/bugs/closed/shouldsucceed/1912.v
index 987a541778..987a541778 100644
--- a/test-suite/bugs/closed/shouldsucceed/bug1912.v
+++ b/test-suite/bugs/closed/shouldsucceed/1912.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2467.v b/test-suite/bugs/closed/shouldsucceed/2467.v
new file mode 100644
index 0000000000..ad17814a8f
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2467.v
@@ -0,0 +1,49 @@
+(*
+In the code below, I would expect the
+    NameSetDec.fsetdec.
+to solve the Lemma, but I need to do it in steps instead.
+
+This is a regression relative to FSet,
+
+I have v8.3 (13702).
+*)
+
+Require Import Coq.MSets.MSets.
+
+Parameter Name : Set.
+Parameter Name_compare : Name -> Name -> comparison.
+Parameter Name_compare_sym : forall {x y : Name},
+                             Name_compare y x = CompOpp (Name_compare x y).
+Parameter Name_compare_trans : forall {c : comparison}
+                                      {x y z : Name},
+                               Name_compare x y = c
+                            -> Name_compare y z = c
+                            -> Name_compare x z = c.
+Parameter Name_eq_leibniz : forall {s s' : Name},
+                            Name_compare s s' = Eq
+                         -> s = s'.
+
+Module NameOrderedTypeAlt.
+Definition t := Name.
+Definition compare := Name_compare.
+Definition compare_sym := @Name_compare_sym.
+Definition compare_trans := @Name_compare_trans.
+End NameOrderedTypeAlt.
+
+Module NameOrderedType := OT_from_Alt(NameOrderedTypeAlt).
+
+Module NameOrderedTypeWithLeibniz.
+Include NameOrderedType.
+Definition eq_leibniz := @Name_eq_leibniz.
+End NameOrderedTypeWithLeibniz.
+
+Module NameSetMod := MSetList.MakeWithLeibniz(NameOrderedTypeWithLeibniz).
+Module NameSetDec := WDecide (NameSetMod).
+
+Lemma foo : forall (xs ys : NameSetMod.t)
+                   (n : Name)
+                   (H1 : NameSetMod.Equal xs (NameSetMod.add n ys)),
+            NameSetMod.In n xs.
+Proof.
+NameSetDec.fsetdec.
+Qed.