diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarsolve.ml | 6 | ||||
| -rw-r--r-- | pretyping/inferCumulativity.ml | 4 |
2 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 96213af9c6..4692fe0057 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -66,9 +66,9 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) if not onlyalg then refresh_sort status ~direction s else t | UnivFlexible alg -> - if onlyalg && alg then - (evdref := Evd.make_flexible_variable !evdref ~algebraic:false l; t) - else t)) + (if alg then + evdref := Evd.make_nonalgebraic_variable !evdref l); + t)) | Set when refreshset && not direction -> (* Cannot make a universe "lower" than "Set", only refreshing when we want higher universes. *) diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index 422a05c19a..9762d0f1d9 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -188,7 +188,7 @@ let infer_inductive env mie = match mie.mind_entry_universes with | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ as univs -> univs - | Cumulative_ind_entry cumi -> + | Cumulative_ind_entry (nas, cumi) -> let uctx = CumulativityInfo.univ_context cumi in let uarray = Instance.to_array @@ UContext.instance uctx in let env = Environ.push_context uctx env in @@ -207,6 +207,6 @@ let infer_inductive env mie = entries in let variances = Array.map (fun u -> LMap.find u variances) uarray in - Cumulative_ind_entry (CumulativityInfo.make (uctx, variances)) + Cumulative_ind_entry (nas, CumulativityInfo.make (uctx, variances)) in { mie with mind_entry_universes = univs } |