diff options
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 2dd3721980..44bfe4b6cc 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -46,7 +46,8 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) (* direction: true for fresh universes lower than the existing ones *) let refresh_sort status ~direction s = let s = ESorts.kind !evdref s in - let s' = evd_comb0 (new_sort_variable status) evdref in + let sigma, s' = new_sort_variable status !evdref in + evdref := sigma; let evd = if direction then set_leq_sort env !evdref s' s else set_leq_sort env !evdref s s' @@ -1690,8 +1691,6 @@ let reconsider_unif_constraints conv_algo evd = (Success evd) pbs -let reconsider_conv_pbs = reconsider_unif_constraints - (* Tries to solve problem t1 = t2. * Precondition: t1 is an uninstantiated evar * Returns an optional list of evars that were instantiated, or None |