diff options
| author | Matthieu Sozeau | 2015-11-26 14:19:37 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-12-01 11:34:54 +0100 |
| commit | f7030a3358dda9bbc6de8058ab3357be277c031a (patch) | |
| tree | bb60d9071da2c8641eadd9b42c0ebf330d9027be /engine/uState.ml | |
| parent | d43915ae5ca44ad0f41a8accd9ab908779f382e5 (diff) | |
Remove unneeded fixpoint in normalize_context_set. Note that it is no
longer stable w.r.t. equality constraints as the universe graph will
choose different canonical levels depending on the equalities given to
it (l = r vs r = l).
Diffstat (limited to 'engine/uState.ml')
| -rw-r--r-- | engine/uState.ml | 30 |
1 files changed, 14 insertions, 16 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index c1aa75c091..75c03bc89c 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -434,23 +434,21 @@ let refresh_undefined_univ_variables uctx = uctx', subst let normalize uctx = - let rec fixpoint uctx = - let ((vars',algs'), us') = - Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables - uctx.uctx_univ_algebraic + let ((vars',algs'), us') = + Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables + uctx.uctx_univ_algebraic + in + if Univ.ContextSet.equal us' uctx.uctx_local then uctx + else + let us', universes = + Universes.refresh_constraints uctx.uctx_initial_universes us' in - if Univ.ContextSet.equal us' uctx.uctx_local then uctx - else - let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in - let uctx' = - { uctx_names = uctx.uctx_names; - uctx_local = us'; - uctx_univ_variables = vars'; - uctx_univ_algebraic = algs'; - uctx_universes = universes; - uctx_initial_universes = uctx.uctx_initial_universes } - in fixpoint uctx' - in fixpoint uctx + { uctx_names = uctx.uctx_names; + uctx_local = us'; + uctx_univ_variables = vars'; + uctx_univ_algebraic = algs'; + uctx_universes = universes; + uctx_initial_universes = uctx.uctx_initial_universes } let universe_of_name uctx s = UNameMap.find s (fst uctx.uctx_names) |