aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/unification.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/unification.ml')
-rw-r--r--pretyping/unification.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 58296002f..4ad8f833e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -936,7 +936,7 @@ let w_coerce env evd mv c =
w_coerce_to_type env evd c cty mvty
let unify_to_type env sigma flags c status u =
- let sigma, c = refresh_universes false sigma c in
+ let sigma, c = refresh_universes false env sigma c in
let t = get_type_of env sigma (nf_meta sigma c) in
let t = nf_betaiota sigma (nf_meta sigma t) in
unify_0 env sigma CUMUL flags t u