From bb7e5aa54afa577da7661fb43cefc9711ccfe4af Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 4 Jun 2012 14:45:54 +0000
Subject: Forward-port fixes from 8.4 (15358, 15353, 15333).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15418 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 5a8dcac080..3047126755 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1854,7 +1854,7 @@ let interp_rawcontext_gen understand_type understand_judgment env bl =
 		(push_rel d env, d::params, succ n, impls)
 	  | Some b ->
 	      let c = understand_judgment env b in
-	      let d = (na, Some c.uj_val, c.uj_type) in
+	      let d = (na, Some c.uj_val, Termops.refresh_universes c.uj_type) in
 		(push_rel d env, d::params, succ n, impls))
       (env,[],1,[]) (List.rev bl)
   in (env, par), impls
-- 
cgit v1.2.3