diff options
| author | Hugo Herbelin | 2015-11-25 17:33:24 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-11-25 17:35:43 +0100 |
| commit | e92aeed3abcf7d42045deb9fb3a450d3527eadc9 (patch) | |
| tree | 7609b2a7c330394819f8f8f9d7d176983638dbd8 | |
| parent | 6f9cc3aca5bb0e5684268a7283796a9272ed5f9d (diff) | |
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).
| -rw-r--r-- | pretyping/retyping.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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) && |