4 files changed, 40 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v
new file mode 100644
index 0000000000..ed44437861
--- /dev/null
+++ b/test-suite/bugs/closed/4782.v
@@ -0,0 +1,9 @@
+(* About typing of with bindings *)
+
+Record r : Type := mk_r { type : Type; cond : type -> Prop }.
+
+Inductive p : Prop := consp : forall (e : r) (x : type e), cond e x -> p.
+
+Goal p.
+Fail apply consp with (fun _ : bool => mk_r unit (fun x => True)) nil.
+ 
diff --git a/test-suite/bugs/closed/4813.v b/test-suite/bugs/closed/4813.v
new file mode 100644
index 0000000000..5f8ea74c1a
--- /dev/null
+++ b/test-suite/bugs/closed/4813.v
@@ -0,0 +1,9 @@
+(* On the strength of "apply with" (see also #4782) *)
+
+Record ProverT := { Facts : Type }.
+Record ProverT_correct (P : ProverT) :=  { Valid : Facts P -> Prop ;
+                                           Valid_weaken : Valid = Valid }.
+Definition reflexivityValid (_ : unit) := True.
+Definition reflexivityProver_correct : ProverT_correct {| Facts := unit |}.
+Proof.
+    eapply Build_ProverT_correct with (Valid := reflexivityValid).
diff --git a/test-suite/bugs/closed/4816.v b/test-suite/bugs/closed/4816.v
new file mode 100644
index 0000000000..86597c88fa
--- /dev/null
+++ b/test-suite/bugs/closed/4816.v
@@ -0,0 +1,17 @@
+Section foo.
+Polymorphic Universes A B.
+Fail Constraint A <= B.
+End foo.
+(* gives an anomaly Universe undefined *)
+
+Universes X Y.
+Section Foo.
+  Polymorphic Universes Z W.
+  Polymorphic Constraint W < Z.
+
+  Fail Definition bla := Type@{W}.
+  Polymorphic Definition bla := Type@{W}.
+  Section Bar.
+    Fail Constraint X <= Z.
+  End Bar.
+End Foo.
diff --git a/test-suite/bugs/opened/4813.v b/test-suite/bugs/opened/4813.v
new file mode 100644
index 0000000000..7c65accfea
--- /dev/null
+++ b/test-suite/bugs/opened/4813.v
@@ -0,0 +1,5 @@
+(* An example one would like to see succeeding *)
+
+Record T := BT { t : Set }.
+Record U (x : T) := BU { u : t x -> Prop }.
+Definition A (H : unit -> Prop) : U (BT unit) := BU _ H.