Imported Upstream version 8.3.pl3upstream/8.3.pl3

1 files changed, 49 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/2467.v b/test-suite/bugs/closed/shouldsucceed/2467.v
new file mode 100644
index 00000000..ad17814a
--- /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.