aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed')
-rw-r--r--test-suite/bugs/closed/2417.v15
-rw-r--r--test-suite/bugs/closed/2640.v17
-rw-r--r--test-suite/bugs/closed/3612.v3
-rw-r--r--test-suite/bugs/closed/3649.v2
-rw-r--r--test-suite/bugs/closed/4121.v4
-rw-r--r--test-suite/bugs/closed/4527.v1
-rw-r--r--test-suite/bugs/closed/4533.v3
-rw-r--r--test-suite/bugs/closed/4544.v3
-rw-r--r--test-suite/bugs/closed/5219.v10
-rw-r--r--test-suite/bugs/closed/5277.v11
-rw-r--r--test-suite/bugs/closed/5321.v18
-rw-r--r--test-suite/bugs/closed/5359.v218
-rw-r--r--test-suite/bugs/closed/5449.v6
-rw-r--r--test-suite/bugs/closed/5476.v28
-rw-r--r--test-suite/bugs/closed/5501.v21
15 files changed, 340 insertions, 20 deletions
diff --git a/test-suite/bugs/closed/2417.v b/test-suite/bugs/closed/2417.v
new file mode 100644
index 000000000..b2f00ffc6
--- /dev/null
+++ b/test-suite/bugs/closed/2417.v
@@ -0,0 +1,15 @@
+Parameter x y : nat.
+Axiom H : x = y.
+Hint Rewrite H : mybase.
+
+Ltac bar base := autorewrite with base.
+
+Tactic Notation "foo" ident(base) := autorewrite with base.
+
+Goal x = 0.
+ bar mybase.
+ now_show (y = 0).
+ Undo 2.
+ foo mybase.
+ now_show (y = 0).
+Abort.
diff --git a/test-suite/bugs/closed/2640.v b/test-suite/bugs/closed/2640.v
deleted file mode 100644
index da0cc68a4..000000000
--- a/test-suite/bugs/closed/2640.v
+++ /dev/null
@@ -1,17 +0,0 @@
-(* Testing consistency of globalization and interpretation in some
- extreme cases *)
-
-Section sect.
-
- (* Simplification of the initial example *)
- Hypothesis Other: True.
-
- Lemma C2 : True.
- proof.
- Fail have True using Other.
- Abort.
-
- (* Variant of the same problem *)
- Lemma C2 : True.
- Fail clear; Other.
- Abort.
diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v
index 90182a488..73709268a 100644
--- a/test-suite/bugs/closed/3612.v
+++ b/test-suite/bugs/closed/3612.v
@@ -38,8 +38,11 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P)
(s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2),
p = q.
+Declare ML Module "ltac_plugin".
Declare ML Module "coretactics".
+Set Default Proof Mode "Classic".
+
Goal forall (A : Type) (B : forall _ : A, Type) (x : @sigT A (fun x : A => B x))
(xx : @paths (@sigT A (fun x0 : A => B x0)) x x),
@paths (@paths (@sigT A (fun x0 : A => B x0)) x x) xx
diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v
index 367d380ec..179f81e66 100644
--- a/test-suite/bugs/closed/3649.v
+++ b/test-suite/bugs/closed/3649.v
@@ -2,7 +2,9 @@
(* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *)
(* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0
coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *)
+Declare ML Module "ltac_plugin".
Declare ML Module "coretactics".
+Set Default Proof Mode "Classic".
Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
Reserved Notation "x = y" (at level 70, no associativity).
Delimit Scope type_scope with type.
diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v
index a8bf950ff..b23684671 100644
--- a/test-suite/bugs/closed/4121.v
+++ b/test-suite/bugs/closed/4121.v
@@ -4,6 +4,8 @@ Unset Strict Universe Declaration.
(* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0
coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (8dbfee5c5f897af8186cb1bdfb04fd4f88eca677) *)
+Declare ML Module "ltac_plugin".
+
Set Universe Polymorphism.
Class Contr_internal (A : Type) := BuildContr { center : A }.
Arguments center A {_}.
@@ -13,4 +15,4 @@ Definition contr_paths_contr0 {A} `{Contr A} : Contr A := {| center := center A
Instance contr_paths_contr1 {A} `{Contr A} : Contr A := {| center := center A |}.
Check @contr_paths_contr0@{i}.
Check @contr_paths_contr1@{i}. (* Error: Universe instance should have length 2 *)
-(** It should have length 1, just like contr_paths_contr0 *) \ No newline at end of file
+(** It should have length 1, just like contr_paths_contr0 *)
diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v
index 4fab9d44f..117d6523a 100644
--- a/test-suite/bugs/closed/4527.v
+++ b/test-suite/bugs/closed/4527.v
@@ -5,6 +5,7 @@ then from 269 lines to 255 lines *)
(* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml
4.01.0
coqtop version 8.5 (January 2016) *)
+Declare ML Module "ltac_plugin".
Inductive False := .
Axiom proof_admitted : False.
Tactic Notation "admit" := case proof_admitted.
diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v
index ccef1c304..c3e0da111 100644
--- a/test-suite/bugs/closed/4533.v
+++ b/test-suite/bugs/closed/4533.v
@@ -5,6 +5,7 @@ then from 285 lines to 271 lines *)
(* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml
4.01.0
coqtop version 8.5 (January 2016) *)
+Declare ML Module "ltac_plugin".
Inductive False := .
Axiom proof_admitted : False.
Tactic Notation "admit" := case proof_admitted.
@@ -223,4 +224,4 @@ v = _) r,
| [ |- p2 @ p0 @ p1 @ eissect (to O A) (g x) = r ] => idtac "good"
| [ |- ?G ] => fail 1 "bad" G
end.
- Fail rewrite concat_p_pp. \ No newline at end of file
+ Fail rewrite concat_p_pp.
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v
index 82f1e3fe7..4ad53bc62 100644
--- a/test-suite/bugs/closed/4544.v
+++ b/test-suite/bugs/closed/4544.v
@@ -2,6 +2,7 @@
(* File reduced by coq-bug-finder from original input, then from 2553 lines to 1932 lines, then from 1946 lines to 1932 lines, then from 2467 lines to 1002 lines, then from 1016 lines to 1002 lines *)
(* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0
coqtop version 8.5 (January 2016) *)
+Declare ML Module "ltac_plugin".
Inductive False := .
Axiom proof_admitted : False.
Tactic Notation "admit" := case proof_admitted.
@@ -1004,4 +1005,4 @@ Proof.
Fail Timeout 1 Time rewrite !loops_functor_group.
(* 0.004 s in 8.5rc1, 8.677 s in 8.5 *)
Timeout 1 do 3 rewrite loops_functor_group.
-Abort. \ No newline at end of file
+Abort.
diff --git a/test-suite/bugs/closed/5219.v b/test-suite/bugs/closed/5219.v
new file mode 100644
index 000000000..f7cec1a0c
--- /dev/null
+++ b/test-suite/bugs/closed/5219.v
@@ -0,0 +1,10 @@
+(* Test surgical use of beta-iota in the type of variables coming from
+ pattern-matching for refine *)
+
+Goal forall x : sigT (fun x => x = 1), True.
+ intro x; refine match x with
+ | existT _ x' e' => _
+ end.
+ lazymatch goal with
+ | [ H : _ = _ |- _ ] => idtac
+ end.
diff --git a/test-suite/bugs/closed/5277.v b/test-suite/bugs/closed/5277.v
new file mode 100644
index 000000000..7abc38bfc
--- /dev/null
+++ b/test-suite/bugs/closed/5277.v
@@ -0,0 +1,11 @@
+(* Scheme Equality not robust wrt names *)
+
+Module A1.
+ Inductive A (T : Type) := C (a : T).
+ Scheme Equality for A. (* success *)
+End A1.
+
+Module A2.
+ Inductive A (x : Type) := C (a : x).
+ Scheme Equality for A.
+End A2.
diff --git a/test-suite/bugs/closed/5321.v b/test-suite/bugs/closed/5321.v
new file mode 100644
index 000000000..03514e23b
--- /dev/null
+++ b/test-suite/bugs/closed/5321.v
@@ -0,0 +1,18 @@
+Definition proj1_sig_path {A} {P : A -> Prop} {u v : sig P} (p : u = v)
+ : proj1_sig u = proj1_sig v
+ := f_equal (@proj1_sig _ _) p.
+
+Definition proj2_sig_path {A} {P : A -> Prop} {u v : sig P} (p : u = v)
+ : eq_rect _ _ (proj2_sig u) _ (proj1_sig_path p) = proj2_sig v
+ := match p with eq_refl => eq_refl end.
+
+Goal forall sz : nat,
+ let sz' := sz in
+ forall pf : sz = sz',
+ let feq_refl := exist (fun x : nat => sz = x) sz' eq_refl in
+ let fpf := exist (fun x : nat => sz = x) sz' pf in feq_refl = fpf ->
+proj2_sig feq_refl = proj2_sig fpf.
+Proof.
+ intros.
+ etransitivity; [ | exact (proj2_sig_path H) ].
+ Fail clearbody fpf.
diff --git a/test-suite/bugs/closed/5359.v b/test-suite/bugs/closed/5359.v
new file mode 100644
index 000000000..87e69565e
--- /dev/null
+++ b/test-suite/bugs/closed/5359.v
@@ -0,0 +1,218 @@
+Require Import Coq.nsatz.Nsatz.
+Goal False.
+
+ (* the first (succeeding) goal was reached by clearing one hypothesis in the second goal which overflows 6GB of stack space *)
+ let sugar := constr:( 0%Z ) in
+ let nparams := constr:( (-1)%Z ) in
+ let reified_goal := constr:(
+ (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2))
+ (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3))
+ (Ring_polynom.PEX Z 6))) ) in
+ let power := constr:( N.one ) in
+ let reified_givens := constr:(
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2))
+ (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3))
+ (Ring_polynom.PEX Z 6)))
+ (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2))
+ (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3))
+ (Ring_polynom.PEX Z 6)))
+ :: Ring_polynom.PEsub
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5))
+ (Ring_polynom.PEX Z 3)) (Ring_polynom.PEX Z 6)))
+ (Ring_polynom.PEX Z 10)) (Ring_polynom.PEc 1%Z)
+ :: Ring_polynom.PEsub
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5))
+ (Ring_polynom.PEX Z 3)) (Ring_polynom.PEX Z 6)))
+ (Ring_polynom.PEX Z 9)) (Ring_polynom.PEc 1%Z)
+ :: Ring_polynom.PEsub
+ (Ring_polynom.PEadd
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 1)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 7)
+ (Ring_polynom.PEX Z 7)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 8) (Ring_polynom.PEX Z 8)))
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 7)
+ (Ring_polynom.PEX Z 7)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 8)
+ (Ring_polynom.PEX Z 8))))
+ :: Ring_polynom.PEsub
+ (Ring_polynom.PEadd
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 1)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 5)
+ (Ring_polynom.PEX Z 5)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 6)
+ (Ring_polynom.PEX Z 6)))
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 5)
+ (Ring_polynom.PEX Z 5)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 6)
+ (Ring_polynom.PEX Z 6))))
+ :: Ring_polynom.PEsub
+ (Ring_polynom.PEadd
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 1)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 2)
+ (Ring_polynom.PEX Z 2)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 3)
+ (Ring_polynom.PEX Z 3)))
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 2)
+ (Ring_polynom.PEX Z 2)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 3)
+ (Ring_polynom.PEX Z 3)))) :: nil)%list ) in
+ Nsatz.nsatz_compute
+ (@cons _ (@Ring_polynom.PEc _ sugar) (@cons _ (@Ring_polynom.PEc _ nparams) (@cons _ (@Ring_polynom.PEpow _ reified_goal power) reified_givens))).
+
+ let sugar := constr:( 0%Z ) in
+ let nparams := constr:( (-1)%Z ) in
+ let reified_goal := constr:(
+ (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2))
+ (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3))
+ (Ring_polynom.PEX Z 6))) ) in
+ let power := constr:( N.one ) in
+ let reified_givens := constr:(
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2))
+ (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3))
+ (Ring_polynom.PEX Z 6)))
+ (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2))
+ (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3))
+ (Ring_polynom.PEX Z 6)))
+ :: Ring_polynom.PEadd
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5))
+ (Ring_polynom.PEX Z 3)) (Ring_polynom.PEX Z 6)))
+ (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5))
+ (Ring_polynom.PEX Z 3)) (Ring_polynom.PEX Z 6))))
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEadd
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 2)
+ (Ring_polynom.PEX Z 6))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 3)
+ (Ring_polynom.PEX Z 5)))) (Ring_polynom.PEX Z 7))
+ (Ring_polynom.PEsub
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 3) (Ring_polynom.PEX Z 6))
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 1)
+ (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5))))
+ (Ring_polynom.PEX Z 8))
+ :: Ring_polynom.PEsub
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5))
+ (Ring_polynom.PEX Z 3)) (Ring_polynom.PEX Z 6)))
+ (Ring_polynom.PEX Z 10)) (Ring_polynom.PEc 1%Z)
+ :: Ring_polynom.PEsub
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEX Z 2))
+ (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3))
+ (Ring_polynom.PEX Z 6))) (Ring_polynom.PEX Z 9))
+ (Ring_polynom.PEc 1%Z)
+ :: Ring_polynom.PEsub
+ (Ring_polynom.PEadd
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 1)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 7)
+ (Ring_polynom.PEX Z 7)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 8)
+ (Ring_polynom.PEX Z 8)))
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 7)
+ (Ring_polynom.PEX Z 7)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 8)
+ (Ring_polynom.PEX Z 8))))
+ :: Ring_polynom.PEsub
+ (Ring_polynom.PEadd
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 1)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 5)
+ (Ring_polynom.PEX Z 5)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 6)
+ (Ring_polynom.PEX Z 6)))
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 5)
+ (Ring_polynom.PEX Z 5)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 6)
+ (Ring_polynom.PEX Z 6))))
+ :: Ring_polynom.PEsub
+ (Ring_polynom.PEadd
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 1)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 2)
+ (Ring_polynom.PEX Z 2)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 3)
+ (Ring_polynom.PEX Z 3)))
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 2)
+ (Ring_polynom.PEX Z 2)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 3)
+ (Ring_polynom.PEX Z 3)))) :: nil)%list ) in
+ Nsatz.nsatz_compute
+ (@cons _ (@Ring_polynom.PEc _ sugar) (@cons _ (@Ring_polynom.PEc _ nparams) (@cons _ (@Ring_polynom.PEpow _ reified_goal power) reified_givens))).
diff --git a/test-suite/bugs/closed/5449.v b/test-suite/bugs/closed/5449.v
new file mode 100644
index 000000000..d7fc2aaa0
--- /dev/null
+++ b/test-suite/bugs/closed/5449.v
@@ -0,0 +1,6 @@
+(* An example of decide equality which was failing due to a lhs dep into the rhs *)
+
+Require Import Coq.PArith.BinPos.
+Goal forall x y, {Pos.compare_cont Gt x y = Gt} + {Pos.compare_cont Gt x y <> Gt}.
+intros.
+decide equality.
diff --git a/test-suite/bugs/closed/5476.v b/test-suite/bugs/closed/5476.v
new file mode 100644
index 000000000..b2d9d943b
--- /dev/null
+++ b/test-suite/bugs/closed/5476.v
@@ -0,0 +1,28 @@
+Require Setoid.
+
+Goal forall (P : Prop) (T : Type) (m m' : T) (T0 T1 : Type) (P2 : forall _ :
+Prop, Prop)
+ (P0 : Set) (x0 : P0) (P1 : forall (_ : P0) (_ : T), Prop)
+ (P3 : forall (_ : forall (_ : P0) (_ : T0) (_ : Prop), Prop) (_ :
+T) (_ : Prop), Prop)
+ (o : forall _ : P0, option T1)
+ (_ : P3
+ (fun (k : P0) (_ : T0) (_ : Prop) =>
+ match o k return Prop with
+ | Some _ => True
+ | None => False
+ end) m' P) (_ : P2 (P1 x0 m))
+ (_ : forall (f : forall (_ : P0) (_ : T0) (_ : Prop), Prop) (m1 m2
+: T)
+ (k : P0) (e : T0) (_ : P2 (P1 k m1)), iff (P3 f m2 P)
+(f k e (P3 f m1 P))), False.
+Proof.
+ intros ???????????? H0 H H1.
+ rewrite H1 in H0; eauto with nocore.
+ { lazymatch goal with
+ | H : match ?X with _ => _ end |- _
+ => first [ lazymatch goal with
+ | [ H' : context[X] |- _ ] => idtac H
+ end
+ | fail 1 "could not find" X ]
+ end.
diff --git a/test-suite/bugs/closed/5501.v b/test-suite/bugs/closed/5501.v
new file mode 100644
index 000000000..24739a365
--- /dev/null
+++ b/test-suite/bugs/closed/5501.v
@@ -0,0 +1,21 @@
+Set Universe Polymorphism.
+
+Record Pred@{A} :=
+ { car :> Type@{A}
+ ; P : car -> Prop
+ }.
+
+Class All@{A} (A : Pred@{A}) : Type :=
+ { proof : forall (a : A), P A a
+ }.
+
+Record Pred_All@{A} : Type :=
+ { P' :> Pred@{A}
+ ; P'_All : All P'
+ }.
+
+Global Instance Pred_All_instance (A : Pred_All) : All A := P'_All A.
+
+Definition Pred_All_proof {A : Pred_All} (a : A) : P A a.
+Proof.
+solve[auto using proof].
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 21:11:28 +0000