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/uState.ml | |
| parent | 5d926b0279f70250db1ee54edcdb4e855ac96f0f (diff) | |
Rename some universe minimizing "normalize" functions to "minimize"
UState normalize -> minimize, Evd nf_constraints -> minimize_universes
Diffstat (limited to 'engine/uState.ml')
| -rw-r--r-- | engine/uState.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index 67479351a..e57afd743 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -585,7 +585,7 @@ let refresh_undefined_univ_variables uctx = uctx_initial_universes = initial } in uctx', subst -let normalize uctx = +let minimize uctx = let ((vars',algs'), us') = Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables uctx.uctx_univ_algebraic @@ -613,3 +613,6 @@ let update_sigma_env uctx env = uctx_universes = univs } in merge true univ_rigid eunivs eunivs.uctx_local + +(** Deprecated *) +let normalize = minimize |