Fix semantics of change p with c to typecheck c at each specific occurrence of p,

avoiding unwanted universe constraints in presence of universe polymorphic constants.
Fixing HoTT bugs # 36, 54 and 113.

1 files changed, 2 insertions, 2 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_054.v b/test-suite/bugs/closed/HoTT_coq_054.v
index f79fe1c1e..b47bb3a20 100644
--- a/test-suite/bugs/closed/HoTT_coq_054.v
+++ b/test-suite/bugs/closed/HoTT_coq_054.v
@@ -47,10 +47,10 @@ Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
                          | inl y' => ap g
                          | inr y' => idmap
                        end
-           | inr x' => match y as y return match y with
+           | inr x' => match y as y return match y return Type with
                                                inr y' => x' = y'
                                              | _ => Empty
-                                           end -> match f y with
+                                           end -> match f y return Type with
                                                     | inr y' => h x' = y'
                                                     | _ => Empty end with
                          | inl y' => idmap