From 07e96102047f55be45bcb2e0a72ac3c764e398b1 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 30 Sep 2015 18:40:20 +0200
Subject: Univs: minor fixes to test-suite files

108 used an implicit lowering to Prop.
---
 test-suite/bugs/closed/HoTT_coq_053.v | 2 +-
 test-suite/bugs/closed/HoTT_coq_093.v | 2 +-
 test-suite/bugs/closed/HoTT_coq_108.v | 2 +-
 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 a14fb6aa57..e2bf1dbedb 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 38943ab353..f382dac976 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 4f5ef99740..b6c0da76ba 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 }
-- 
cgit v1.2.3