diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-04-08 18:01:28 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:59:00 +0200 |
| commit | b6cf2215494165d3d1089881b3566ad8a153f33a (patch) | |
| tree | 1d8b935f34e28d9d0e29699a92a2100a42f25897 | |
| parent | be428c80f7be97b80e7e1e58d195a26465407915 (diff) | |
Proper calculation of constructor levels, forgetting the level of lets.
| -rw-r--r-- | toplevel/command.ml | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 6866bc69e..f4171da1b 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -341,12 +341,15 @@ let interp_cstrs evdref env impls mldata arity ind = let sign_level env evd sign = fst (List.fold_right - (fun (_,_,t as d) (lev,env) -> - let s = destSort (Reduction.whd_betadeltaiota env - (nf_evar evd (Retyping.get_type_of env evd t))) - in - let u = univ_of_sort s in - (Univ.sup u lev, push_rel d env)) + (fun (_,b,t as d) (lev,env) -> + match b with + | Some _ -> (lev, push_rel d env) + | None -> + let s = destSort (Reduction.whd_betadeltaiota env + (nf_evar evd (Retyping.get_type_of env evd t))) + in + let u = univ_of_sort s in + (Univ.sup u lev, push_rel d env)) sign (Univ.type0m_univ,env)) let sup_list = List.fold_left Univ.sup Univ.type0m_univ |