From 0fcf7621f45a20765dbc7e39973abe78610dca64 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 27 Jun 2006 21:29:18 +0000
Subject: Correction bug #1182 (ajout refresh_universe car le polymorphisme de
 sorte des inductifs maintenant retourne des sortes d'inductives qui ne sont
 pas des variables) et test de non-régression

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

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index be24d22b59..8b41b9c9b5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -482,6 +482,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		       else
 			 error_cant_find_case_type_loc loc env (evars_of !isevars) 
 			   cj.uj_val in
+		     let ccl = refresh_universes ccl in
 		     let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
 		     let v =
 		       let mis,_ = dest_ind_family indf in
-- 
cgit v1.2.3