diff options
| author | Gaëtan Gilbert | 2017-10-12 13:55:08 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 13:27:38 +0100 |
| commit | a0e16c9e5c3f88a8b72935dd4877f13388640f69 (patch) | |
| tree | b177cc86b2742893adf0b181e53c03b8897b48cc /pretyping/evardefine.ml | |
| parent | 6c447d7a7190857b03bb2992f443f1b818618a94 (diff) | |
Make Sorts.t private
Diffstat (limited to 'pretyping/evardefine.ml')
| -rw-r--r-- | pretyping/evardefine.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index a62427834d..55dfdc0574 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -97,7 +97,7 @@ let define_pure_evar_as_product evd evk = new_type_evar newenv evd1 status ~src ~filter in let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in - let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) (ESorts.kind evd1 s) in + let evd3 = Evd.set_leq_sort evenv evd3 (Sorts.sort_of_univ prods) (ESorts.kind evd1 s) in evd3, rng in let prod = mkProd (Name id, dom, subst_var id rng) in @@ -164,13 +164,12 @@ let rec evar_absorb_arguments env evd (evk,args as ev) = function (* Refining an evar to a sort *) let define_evar_as_sort env evd (ev,args) = - let evd, u = new_univ_variable univ_rigid evd in + let evd, s = new_sort_variable univ_rigid evd in let evi = Evd.find_undefined evd ev in - let s = Type u in let concl = Reductionops.whd_all (evar_env evi) evd evi.evar_concl in let sort = destSort evd concl in let evd' = Evd.define ev (mkSort s) evd in - Evd.set_leq_sort env evd' (Type (Univ.super u)) (ESorts.kind evd' sort), s + Evd.set_leq_sort env evd' (Sorts.super s) (ESorts.kind evd' sort), s (* Propagation of constraints through application and abstraction: Given a type constraint on a functional term, returns the type |