diff options
| author | Pierre-Marie Pédrot | 2017-12-13 17:33:04 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-12-30 19:23:04 +0100 |
| commit | bad3f3b784d3de8851615b8f4b7afba734232d8e (patch) | |
| tree | be6a12a50d3bf6b73ea7866334585f694370e630 /engine/evd.ml | |
| parent | 441bea723c511ed9e18ef005678bd01242b45c49 (diff) | |
Moving some universe substitution code out of the kernel.
This code was not used at all inside the kernel, it was related to universe
unification that happens in the upper layer. It makes more sense to put it
somewhere upper.
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index e33c851f6e..0e94721589 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -855,7 +855,7 @@ let normalize_universe evd = let normalize_universe_instance evd l = let vars = ref (UState.subst evd.universes) in - let normalize = Univ.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in + let normalize = Universes.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in Univ.Instance.subst_fn normalize l let normalize_sort evars s = |