From d1c9de736aa576ab31a114d65d67db6e10ef8bec Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 7 Oct 2011 11:29:50 +0000
Subject: 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
---
 test-suite/bugs/closed/shouldsucceed/1912.v    |  6 ++++
 test-suite/bugs/closed/shouldsucceed/2467.v    | 49 ++++++++++++++++++++++++++
 test-suite/bugs/closed/shouldsucceed/bug1912.v |  6 ----
 3 files changed, 55 insertions(+), 6 deletions(-)
 create mode 100644 test-suite/bugs/closed/shouldsucceed/1912.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2467.v
 delete mode 100644 test-suite/bugs/closed/shouldsucceed/bug1912.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/shouldsucceed/1912.v b/test-suite/bugs/closed/shouldsucceed/1912.v
new file mode 100644
index 0000000000..987a541778
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1912.v
@@ -0,0 +1,6 @@
+Require Import ZArith.
+
+Goal forall x, Z.succ (Z.pred x) = x.
+intros x.
+omega.
+Qed.
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.
diff --git a/test-suite/bugs/closed/shouldsucceed/bug1912.v b/test-suite/bugs/closed/shouldsucceed/bug1912.v
deleted file mode 100644
index 987a541778..0000000000
--- a/test-suite/bugs/closed/shouldsucceed/bug1912.v
+++ /dev/null
@@ -1,6 +0,0 @@
-Require Import ZArith.
-
-Goal forall x, Z.succ (Z.pred x) = x.
-intros x.
-omega.
-Qed.
-- 
cgit v1.2.3