diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/indrec.ml | 3 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 5 |
2 files changed, 6 insertions, 2 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 996c00ebaf..689257c3b5 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -591,7 +591,8 @@ let lookup_eliminator ind_sp s = errorlabstrm "default_elim" (strbrk "Cannot find the elimination combinator " ++ pr_id id ++ strbrk ", the elimination of the inductive definition " ++ - pr_id id ++ strbrk " on sort " ++ pr_sort_family s ++ + pr_global_env Idset.empty (IndRef ind_sp) ++ + strbrk " on sort " ++ pr_sort_family s ++ strbrk " is probably not allowed.") diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 123ff43e7b..532c258fa1 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -115,8 +115,11 @@ let retype sigma metamap = 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) when isGlobalRef f -> + let t = type_of_global_reference_knowing_parameters env f args in + family_of_sort (sort_of_atomic_type env sigma t args) | App(f,args) -> - family_of_sort (sort_of_atomic_type env sigma (type_of env f) args) + family_of_sort (sort_of_atomic_type env sigma (type_of env f) args) | Lambda _ | Fix _ | Construct _ -> anomaly "sort_of: Not a type (1)" | _ -> family_of_sort (decomp_sort env sigma (type_of env t)) |