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 /engine/evarutil.ml | |
| parent | 5d926b0279f70250db1ee54edcdb4e855ac96f0f (diff) | |
Rename some universe minimizing "normalize" functions to "minimize"
UState normalize -> minimize, Evd nf_constraints -> minimize_universes
Diffstat (limited to 'engine/evarutil.ml')
| -rw-r--r-- | engine/evarutil.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 7674cf67a..6b3ce048f 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -89,15 +89,15 @@ let nf_evars_universes evm = (Evd.universe_subst evm) let nf_evars_and_universes evm = - let evm = Evd.nf_constraints evm in + let evm = Evd.minimize_universes evm in evm, nf_evars_universes evm let e_nf_evars_and_universes evdref = - evdref := Evd.nf_constraints !evdref; + evdref := Evd.minimize_universes !evdref; nf_evars_universes !evdref, Evd.universe_subst !evdref let nf_evar_map_universes evm = - let evm = Evd.nf_constraints evm in + let evm = Evd.minimize_universes evm in let subst = Evd.universe_subst evm in if Univ.LMap.is_empty subst then evm, nf_evar0 evm else |