4 files changed, 149 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 00000000..af708587
--- /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
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.
diff --git a/test-suite/bugs/closed/shouldsucceed/2608.v b/test-suite/bugs/closed/shouldsucceed/2608.v
new file mode 100644
index 00000000..a4c95ff9
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2608.v
@@ -0,0 +1,34 @@
+
+Module Type T.
+  Parameter Inline t : Type.
+End T.
+
+Module M.
+  Definition t := nat.
+End M.
+
+Module Make (X:T).
+  Include X.
+
+  (* here t is : (Top.Make.t,Top.X.t) *)
+
+  (* in libobject HEAD : EvalConstRef (Top.X.t,Top.X.t)
+     which is substituted by : {Top.X |-> Top.Make [, Top.Make.t=>Top.X.t]}
+     which gives : EvalConstRef (Top.Make.t,Top.X.t) *)
+
+End Make.
+
+Module P := Make M.
+
+  (* resolver returned by add_module : Top.P.t=>inline *)
+  (* then constant_of_delta_kn P.t produces (Top.P.t,Top.P.t) *)
+
+  (* in libobject HEAD : EvalConstRef (Top.Make.t,Top.X.t)
+     given to subst = {<X#1> |-> Top.M [, Top.M.t=>inline]}
+     which used to give : EvalConstRef (Top.Make.t,Top.M.t)
+     given to subst = {Top.Make |-> Top.P [, Top.P.t=>inline]}
+     which used to give : EvalConstRef (Top.P.t,Top.M.t) *)
+
+Definition u := P.t.
+ (* was raising Not_found since Heads.head_map knows of (Top.P.t,Top.M.t)
+    and not of (Top.P.t,Top.P.t) *)
diff --git a/test-suite/bugs/closed/shouldsucceed/808_2411.v b/test-suite/bugs/closed/shouldsucceed/808_2411.v
new file mode 100644
index 00000000..1c13e745
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/808_2411.v
@@ -0,0 +1,27 @@
+Section test.
+Variable n:nat.
+Lemma foo: 0 <= n.
+Proof.
+(* declaring an Axiom during a proof makes it immediatly
+   usable, juste as a full Definition. *)
+Axiom bar : n = 1.
+rewrite bar.
+now apply le_S.
+Qed.
+
+Lemma foo' : 0 <= n.
+Proof.
+(* Declaring an Hypothesis during a proof is ok,
+   but this hypothesis won't be usable by the current proof(s),
+   only by later ones. *)
+Hypothesis bar' : n = 1.
+Fail rewrite bar'.
+Abort.
+
+Lemma foo'' : 0 <= n.
+Proof.
+rewrite bar'.
+now apply le_S.
+Qed.
+
+End test.
+\ No newline at end of file