diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-10-11 19:41:23 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-26 13:52:52 +0200 |
| commit | af0a04b8e16c2554e0c747da6d625799b332f5fe (patch) | |
| tree | dc73cbe7d56a1eea7bb7c22ab1576d0ffa673b11 /vernac | |
| parent | a1fc621b943dbf904705dc88ed27c26daf4c5e72 (diff) | |
Remove Sorts.contents
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comInductive.ml | 8 | ||||
| -rw-r--r-- | vernac/record.ml | 3 |
2 files changed, 5 insertions, 6 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 6057c05f5..0387b32ba 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -126,7 +126,7 @@ let make_conclusion_flexible sigma ty poly = else sigma let is_impredicative env u = - u = Prop Null || (is_impredicative_set env && u = Prop Pos) + u = Prop || (is_impredicative_set env && u = Set) let interp_ind_arity env sigma ind = let c = intern_gen IsType env sigma ind.ind_arity in @@ -245,7 +245,7 @@ let solve_constraints_system levels level_bounds = let inductive_levels env evd poly arities inds = let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in let levels = List.map (fun (x,(ctx,a)) -> - if a = Prop Null then None + if a = Prop then None else Some (univ_of_sort a)) destarities in let cstrs_levels, min_levels, sizes = @@ -298,14 +298,14 @@ let inductive_levels env evd poly arities inds = (** "Polymorphic" type constraint and more than one constructor, should not land in Prop. Add constraint only if it would land in Prop directly (no informative arguments as well). *) - Evd.set_leq_sort env evd (Prop Pos) du + Evd.set_leq_sort env evd Set du else evd in let duu = Sorts.univ_of_sort du in let evd = if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then - Evd.set_eq_sort env evd (Prop Null) du + Evd.set_eq_sort env evd Prop du else evd else Evd.set_eq_sort env evd (Type cu) du in diff --git a/vernac/record.ml b/vernac/record.ml index 202c9b92f..2d7800827 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -164,8 +164,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then (* We can assume that the level in aritysort is not constrained and clear it, if it is flexible *) - Evd.set_eq_sort env_ar sigma (Prop Pos) sort, - EConstr.mkSort (Sorts.sort_of_univ univ) + Evd.set_eq_sort env_ar sigma Set sort, EConstr.mkSort (Sorts.sort_of_univ univ) else sigma, typ in let sigma = Evd.minimize_universes sigma in |