diff options
| author | Matthieu Sozeau | 2014-07-11 19:18:39 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-11 19:19:40 +0200 |
| commit | 2b833c49456c52ae941fc87b789e9d520d5b3c40 (patch) | |
| tree | 2c2dfea327c4974969a83b6004dcd0735b04af7d | |
| parent | b56c318f471e3c82cebbd64aa80ceb83e8ae8b63 (diff) | |
Properly add a Set lower bound on any polymorphic inductive in Type with
more than one constructor.
| -rw-r--r-- | kernel/indtypes.ml | 6 | ||||
| -rw-r--r-- | toplevel/command.ml | 8 |
2 files changed, 8 insertions, 6 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index ee4a404a7c..f79d16c02f 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -156,8 +156,10 @@ let infer_constructor_packet env_ar_par ctx params lc = let lc'' = Array.map (fun j -> it_mkProd_or_LetIn j.utj_val params) jlc in (* compute the max of the sorts of the products of the constructors types *) let levels = List.map (infos_and_sort env_ar_par ctx) lc in - let level = List.fold_left (fun max l -> Universe.sup max l) Universe.type0m levels in - (lc'',(is_unit levels,level)) + let isunit = is_unit levels in + let min = if Array.length jlc > 1 then Universe.type0 else Universe.type0m in + let level = List.fold_left (fun max l -> Universe.sup max l) min levels in + (lc'', (isunit, level)) (* If indices matter *) let cumulate_arity_large_levels env sign = diff --git a/toplevel/command.ml b/toplevel/command.ml index ff2e89351e..0e4d6e3306 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -385,13 +385,13 @@ let sign_level env evd sign = (Univ.sup u lev, push_rel d env)) sign (Univ.type0m_univ,env)) -let sup_list = List.fold_left Univ.sup Univ.type0m_univ +let sup_list min = List.fold_left Univ.sup min -let extract_level env evd tys = +let extract_level env evd min tys = let sorts = List.map (fun ty -> let ctx, concl = Reduction.dest_prod_assum env ty in sign_level env evd ((Anonymous, None, concl) :: ctx)) tys - in sup_list sorts + in sup_list min sorts let inductive_levels env evdref poly arities inds = let destarities = List.map (Reduction.dest_arity env) arities in @@ -403,12 +403,12 @@ let inductive_levels env evdref poly arities inds = CList.split3 (List.map2 (fun (_,tys,_) (ctx,du) -> let len = List.length tys in - let clev = extract_level env !evdref tys in let minlev = if len > 1 && not (is_impredicative env du) then Univ.type0_univ else Univ.type0m_univ in + let clev = extract_level env !evdref minlev tys in (clev, minlev, len)) inds destarities) in (* Take the transitive closure of the system of constructors *) |