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 /toplevel | |
| parent | b56c318f471e3c82cebbd64aa80ceb83e8ae8b63 (diff) | |
Properly add a Set lower bound on any polymorphic inductive in Type with
more than one constructor.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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 *) |