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 /plugins | |
| parent | 5d926b0279f70250db1ee54edcdb4e855ac96f0f (diff) | |
Rename some universe minimizing "normalize" functions to "minimize"
UState normalize -> minimize, Evd nf_constraints -> minimize_universes
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 6e38b4641..e0368153e 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1922,7 +1922,7 @@ let build_morphism_signature env sigma m = in let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in let evd = solve_constraints env !evd in - let evd = Evd.nf_constraints evd in + let evd = Evd.minimize_universes evd in let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in Pretyping.check_evars env Evd.empty evd (EConstr.of_constr m); Evd.evar_universe_context evd, m |