From e92aeed3abcf7d42045deb9fb3a450d3527eadc9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 25 Nov 2015 17:33:24 +0100
Subject: Reverting 1467c225 (Fixing an old typo in Retyping, found by Matej).

This was not a typo (was correctly taking the family type of the type).
---
 pretyping/retyping.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index a169a4577e..fb55265526 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -158,7 +158,8 @@ let retype ?(polyprop=true) sigma =
   and sort_family_of env t =
     match kind_of_term t with
     | Cast (c,_, s) when isSort s -> family_of_sort (destSort s)
-    | Sort s -> family_of_sort s
+    | Sort (Prop c) -> InType
+    | Sort (Type u) -> InType
     | Prod (name,t,c2) ->
 	let s2 = sort_family_of (push_rel (name,None,t) env) c2 in
 	if not (is_impredicative_set env) &&
-- 
cgit v1.2.3