From 679f2bb705ca48e708d9f6a66402a2de9748e15d Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Wed, 10 Oct 2018 11:48:23 +0000
Subject: [test-suite] rename a file

---
 test-suite/bugs/closed/5197.v     | 44 ---------------------------------------
 test-suite/bugs/closed/bug_5197.v | 44 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 44 insertions(+), 44 deletions(-)
 delete mode 100644 test-suite/bugs/closed/5197.v
 create mode 100644 test-suite/bugs/closed/bug_5197.v

diff --git a/test-suite/bugs/closed/5197.v b/test-suite/bugs/closed/5197.v
deleted file mode 100644
index b67e93d677..0000000000
--- a/test-suite/bugs/closed/5197.v
+++ /dev/null
@@ -1,44 +0,0 @@
-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/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.
-- 
cgit v1.2.3