From 1467c22548453cd07ceba0029e37c8bbdfd039ea Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 23 Nov 2015 17:51:16 +0100
Subject: Fixing an old typo in Retyping, found by Matej.

---
 pretyping/retyping.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index fb55265526..a169a4577e 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -158,8 +158,7 @@ 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 (Prop c) -> InType
-    | Sort (Type u) -> InType
+    | Sort s -> family_of_sort s
     | 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