diff options
Diffstat (limited to 'pretyping/retyping.ml')
| -rw-r--r-- | pretyping/retyping.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 03afe0a17..123ff43e7 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -111,7 +111,10 @@ let retype sigma metamap = | Cast (c,_, s) when isSort s -> family_of_sort (destSort s) | Sort (Prop c) -> InType | Sort (Type u) -> InType - | Prod (name,t,c2) -> sort_family_of (push_rel (name,None,t) env) c2 + | Prod (name,t,c2) -> + let s2 = sort_family_of (push_rel (name,None,t) env) c2 in + if Environ.engagement env <> Some ImpredicativeSet && + s2 = InSet & sort_family_of env t = InType then InType else s2 | App(f,args) -> family_of_sort (sort_of_atomic_type env sigma (type_of env f) args) | Lambda _ | Fix _ | Construct _ -> |