From b6cf2215494165d3d1089881b3566ad8a153f33a Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 8 Apr 2014 18:01:28 +0200 Subject: Proper calculation of constructor levels, forgetting the level of lets. --- toplevel/command.ml | 15 +++++++++------ 1 file 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 -- cgit v1.2.3