From be428c80f7be97b80e7e1e58d195a26465407915 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 8 Apr 2014 16:58:52 +0200
Subject: Refresh some universes in cases.ml as they might appear in the term.

---
 pretyping/cases.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 2b0a2dda95..75ebdeb22b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1559,6 +1559,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
         map_constr_with_full_binders push_binder aux x t
     | Evar ev ->
         let ty = get_type_of env sigma t in
+	let ty = Evarutil.evd_comb1 (refresh_universes false) evdref ty in
         let inst =
 	  List.map_i
 	    (fun i _ ->
@@ -1574,7 +1575,11 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
       map_constr_with_full_binders push_binder aux x t
     | (_, _, u) :: _ -> (* u is in extenv *)
       let vl = List.map pi1 good in
-      let ty = lift (-k) (aux x (get_type_of env !evdref t)) in
+      let ty = 
+	let ty = get_type_of env !evdref t in
+	  Evarutil.evd_comb1 (refresh_universes false) evdref ty
+      in
+      let ty = lift (-k) (aux x ty) in
       let depvl = free_rels ty in
       let inst =
 	List.map_i
-- 
cgit v1.2.3