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/uState.ml | |
| parent | 6c8b00e47334f60f200256d45a5542fa80ce4b12 (diff) | |
Don't use ref universe_opt_subst
Diffstat (limited to 'engine/uState.ml')
| -rw-r--r-- | engine/uState.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index 6c8dbe3f4..df50bae86 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -156,7 +156,7 @@ let process_universe_constraints ctx cstrs = let univs = ctx.uctx_universes in let vars = ref ctx.uctx_univ_variables in let weak = ref ctx.uctx_weak_constraints in - let normalize = normalize_univ_variable_opt_subst vars in + let normalize u = normalize_univ_variable_opt_subst !vars u in let nf_constraint = function | ULub (u, v) -> ULub (level_subst_of normalize u, level_subst_of normalize v) | UWeak (u, v) -> UWeak (level_subst_of normalize u, level_subst_of normalize v) |