4 files changed, 45 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/bug_4132.v b/test-suite/bugs/closed/bug_4132.v
index 806ffb771f..67ecc3087f 100644
--- a/test-suite/bugs/closed/bug_4132.v
+++ b/test-suite/bugs/closed/bug_4132.v
@@ -26,6 +26,6 @@ Qed.
 
 Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b.
 omega. (* Pierre L: according to a comment of bug report #4132,
-          this might have triggered "Failure(occurence 2)" in the past,
+          this might have triggered "Failure(occurrence 2)" in the past,
           but I never managed to reproduce that. *)
 Qed.
diff --git a/test-suite/bugs/closed/bug_5197.v b/test-suite/bugs/closed/bug_5197.v
new file mode 100644
index 0000000000..b67e93d677
--- /dev/null
+++ b/test-suite/bugs/closed/bug_5197.v
@@ -0,0 +1,44 @@
+Set Universe Polymorphism.
+Set Primitive Projections.
+Unset Printing Primitive Projection Compatibility.
+Axiom Ω : Type.
+
+Record Pack (A : Ω -> Type) (Aᴿ : Ω -> (forall ω : Ω, A ω) -> Type) := mkPack {
+  elt : forall ω, A ω;
+  prp : forall ω, Aᴿ ω elt;
+}.
+
+Record TYPE := mkTYPE {
+  wit : Ω -> Type;
+  rel : Ω -> (forall ω : Ω, wit ω) -> Type;
+}.
+
+Definition El (A : TYPE) : Type := Pack A.(wit) A.(rel).
+
+Definition Typeᶠ : TYPE := {|
+  wit := fun _ => Type;
+  rel := fun _ A => (forall ω : Ω, A ω) -> Type;
+                          |}.
+Set Printing Universes.
+Fail Definition Typeᵇ : El Typeᶠ :=
+  mkPack _ _ (fun w => Type) (fun w A => (forall ω, A ω) -> Type).
+
+Definition Typeᵇ : El Typeᶠ :=
+  mkPack _ (fun _ (A : Ω -> Type) => (forall ω : Ω, A ω) -> _) (fun w => Type) (fun w A => (forall ω, A ω) -> Type).
+
+(** Bidirectional typechecking helps here *)
+Require Import Program.Tactics.
+Program Definition progTypeᵇ : El Typeᶠ :=
+  mkPack _ _ (fun w => Type) (fun w A => (forall ω, A ω) -> Type).
+
+(**
+The command has indeed failed with message:
+Error: Conversion test raised an anomaly
+**)
+
+Definition Typeᵇ' : El Typeᶠ.
+Proof.
+unshelve refine (mkPack _ _ _ _).
++ refine (fun _ => Type).
++ simpl. refine (fun _ A => (forall ω, A ω) -> Type).
+Defined.
diff --git a/test-suite/bugs/closed/8553.v b/test-suite/bugs/closed/bug_8553.v
index 4a1afabe89..4a1afabe89 100644
--- a/test-suite/bugs/closed/8553.v
+++ b/test-suite/bugs/closed/bug_8553.v
diff --git a/test-suite/bugs/closed/8672.v b/test-suite/bugs/closed/bug_8672.v
index 66cd6dfa8c..66cd6dfa8c 100644
--- a/test-suite/bugs/closed/8672.v
+++ b/test-suite/bugs/closed/bug_8672.v