Univs: minor fixes to test-suite files

108 used an implicit lowering to Prop.

3 files changed, 3 insertions, 3 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_053.v b/test-suite/bugs/closed/HoTT_coq_053.v
index a14fb6aa5..e2bf1dbed 100644
--- a/test-suite/bugs/closed/HoTT_coq_053.v
+++ b/test-suite/bugs/closed/HoTT_coq_053.v
@@ -39,7 +39,7 @@ Definition NatCategory (n : nat) :=
 Definition NatCategory' (n : nat) :=
   match n with
     | 0 => (fun X => @Build_PreCategory X
-                         (fun _ _ => Unit : Prop)) Unit
+                         (fun _ _ => Unit : Set)) Unit
     | _ => DiscreteCategory Bool
   end.
 
diff --git a/test-suite/bugs/closed/HoTT_coq_093.v b/test-suite/bugs/closed/HoTT_coq_093.v
index 38943ab35..f382dac97 100644
--- a/test-suite/bugs/closed/HoTT_coq_093.v
+++ b/test-suite/bugs/closed/HoTT_coq_093.v
@@ -21,7 +21,7 @@ Section lift.
   Definition Lift (A : Type@{i}) : Type@{j} := A.
 End lift.
 
-Goal forall (A : Type@{i}) (x y : A), @paths@{i} A x y -> @paths@{j} A x y.
+Goal forall (A : Type@{i}) (x y : A), @paths@{i j} A x y -> @paths@{j k} A x y.
 intros A x y p.
 compute in *. destruct p. exact idpath.
 Defined.
diff --git a/test-suite/bugs/closed/HoTT_coq_108.v b/test-suite/bugs/closed/HoTT_coq_108.v
index 4f5ef9974..b6c0da76b 100644
--- a/test-suite/bugs/closed/HoTT_coq_108.v
+++ b/test-suite/bugs/closed/HoTT_coq_108.v
@@ -107,7 +107,7 @@ Section path_functor.
   Variable D : PreCategory.
   Local Notation path_functor'_T F G
     := { HO : object_of F = object_of G
-       | transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) (GO d))
+       & transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) (GO d))
                    HO
                    (morphism_of F)
          = morphism_of G }