Closed bugs.

3 files changed, 81 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3807.v b/test-suite/bugs/closed/3807.v
new file mode 100644
index 000000000..108ebf592
--- /dev/null
+++ b/test-suite/bugs/closed/3807.v
@@ -0,0 +1,33 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+Unset Universe Minimization ToSet.
+
+
+Definition foo : Type := nat.
+About foo.
+(* foo@{Top.1} : Type@{Top.1}*)
+(* Top.1 |=  *)
+
+Definition bar : foo -> nat.
+Admitted.
+About bar.
+(* bar@{Top.2} : foo@{Top.2} -> nat *)
+(* Top.2 |=  *)
+
+Lemma baz@{i} : foo@{i} -> nat.
+Proof.
+  exact bar.
+Defined.
+
+Definition bar'@{i} : foo@{i} -> nat.
+  intros f. exact 0.
+Admitted.
+About bar'.
+(* bar'@{i} : foo@{i} -> nat *)
+(* i |=  *)
+
+Axiom f@{i} : Type@{i}.
+(*
+*** [ f@{i} : Type@{i} ]
+(* i |=  *)
+*)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4400.v b/test-suite/bugs/closed/4400.v
new file mode 100644
index 000000000..5c23f8404
--- /dev/null
+++ b/test-suite/bugs/closed/4400.v
@@ -0,0 +1,19 @@
+(* -*- coq-prog-args: ("-emacs" "-require" "Coq.Compat.Coq84" "-compat" "8.4") -*- *)
+Require Import Coq.Lists.List Coq.Logic.JMeq Program.Equality.
+Set Printing Universes.
+Inductive Foo (I : Type -> Type) (A : Type) : Type :=
+| foo (B : Type) : A -> I B -> Foo I A.
+Definition Family := Type -> Type.
+Definition FooToo : Family -> Family := Foo.
+Definition optionize (I : Type -> Type) (A : Type) := option (I A).
+Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo(optionize I) A := foo (optionize I) A A.
+Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }.
+Definition barRec : Rec (optionize id) := {| rec := bar id |}.
+Inductive Empty {T} : T -> Prop := .
+Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family)
+nil)) (b : unit) :
+  Empty (a, b) -> False.
+Proof.
+  intro e.
+  dependent induction e.
+Qed.
diff --git a/test-suite/bugs/closed/4433.v b/test-suite/bugs/closed/4433.v
new file mode 100644
index 000000000..9eeb86468
--- /dev/null
+++ b/test-suite/bugs/closed/4433.v
@@ -0,0 +1,29 @@
+Require Import Coq.Arith.Arith Coq.Init.Wf.
+Axiom proof_admitted : False.
+Goal exists x y z : nat, Fix
+                           Wf_nat.lt_wf
+                           (fun _ => nat -> nat)
+                           (fun x' f => match x' as x'0
+                                              return match x'0 with
+                                                       | 0 => True
+                                                       | S x'' => x'' < x'
+                                                     end
+                                                     -> nat -> nat
+                                        with
+                                          | 0 => fun _ _ => 0
+                                          | S x'' => f x''
+                                        end
+                                          (match x' with
+                                             | 0 => I
+                                             | S x'' => (Nat.lt_succ_diag_r _)
+                                           end))
+                           z
+                           y
+                         = 0.
+Proof.
+  do 3 (eexists; [ shelve.. | ]).
+  match goal with |- ?G => let G' := (eval lazy in G) in change G with G' end.
+  case proof_admitted.
+  Unshelve.
+  all:constructor.
+Defined.
\ No newline at end of file