diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-08 12:59:35 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-08 12:59:35 +0200 |
| commit | 96a357777e2e3c1273a61e0767bc04085d56835e (patch) | |
| tree | 0903a7e3054db52c81f2b4c6d54812a8cf6a775f /engine/evd.ml | |
| parent | 6c8b00e47334f60f200256d45a5542fa80ce4b12 (diff) | |
Don't use ref universe_opt_subst
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index af22de5cd..20a7c80ea 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -842,12 +842,12 @@ let universe_rigidity evd l = else UnivRigid let normalize_universe evd = - let vars = ref (UState.subst evd.universes) in + let vars = UState.subst evd.universes in let normalize = Universes.normalize_universe_opt_subst vars in normalize let normalize_universe_instance evd l = - let vars = ref (UState.subst evd.universes) in + let vars = UState.subst evd.universes in let normalize = Universes.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in Univ.Instance.subst_fn normalize l |