summaryrefslogtreecommitdiff
path: root/test-suite/bugs
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs')
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2464.v39
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2467.v49
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2608.v34
-rw-r--r--test-suite/bugs/closed/shouldsucceed/808_2411.v27
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