diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comAssumption.ml | 2 | ||||
| -rw-r--r-- | vernac/comDefinition.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 1712634da..6a590758f 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -160,7 +160,7 @@ let do_assumptions kind nl l = in let sigma = solve_remaining_evars all_and_fail_flags env sigma Evd.empty in (* The universe constraints come from the whole telescope. *) - let sigma = Evd.nf_constraints sigma in + let sigma = Evd.minimize_universes sigma in let nf_evar c = EConstr.to_constr sigma c in let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) -> let t = nf_evar t in diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 01dbe0a0d..b18a60a1f 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -85,7 +85,7 @@ let interp_definition pl bl poly red_option c ctypopt = evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsty, Some ty in (* universe minimization *) - let evd = Evd.nf_constraints evd in + let evd = Evd.minimize_universes evd in (* Substitute evars and universes, and add parameters. Note: in program mode some evars may remain. *) let ctx = List.map (EConstr.to_rel_decl evd) ctx in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 0ff6d9c17..26c6a8cbe 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -72,7 +72,7 @@ let show_top_evars () = let show_universes () = let pfts = Proof_global.give_me_the_proof () in let gls,_,_,_,sigma = Proof.proof pfts in - let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in + let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++ str "Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx |