diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-02 15:10:39 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-06 13:42:31 +0100 |
| commit | 66973ce17e32a3c692a5b0032f38300ec8cc36d3 (patch) | |
| tree | e8c0b4a760bd008afde92ea1902a6e2c2ba3946b /vernac/comAssumption.ml | |
| parent | 5d926b0279f70250db1ee54edcdb4e855ac96f0f (diff) | |
Rename some universe minimizing "normalize" functions to "minimize"
UState normalize -> minimize, Evd nf_constraints -> minimize_universes
Diffstat (limited to 'vernac/comAssumption.ml')
| -rw-r--r-- | vernac/comAssumption.ml | 2 |
1 files changed, 1 insertions, 1 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 |