From 618b18f7ae45c90062e5877cf55025ef5506b9b5 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 19 Sep 2001 17:08:06 +0000
Subject: Blindage, de peur que des types entrant non en forme normale ne
 provoque des calculs sur les univers dans get_sort_family_of

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

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index e4c900b31..5ed6e6051 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -96,7 +96,7 @@ let typeur sigma metamap =
     | _ -> outsort env sigma (type_of env t)
 
   and sort_family_of env t =
-    match kind_of_term t with
+    match kind_of_term (whd_betadeltaiota env sigma t) with
     | IsCast (c,s) when isSort s -> family_of_sort (destSort s)
     | IsSort (Prop c) -> InType
     | IsSort (Type u) -> InType
-- 
cgit v1.2.3