diff options
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 124faf05b..b07bf4f92 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -588,7 +588,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag (try let sigma' = if pb == CUMUL - then Evd.set_leq_sort sigma s1 s2 + then Evd.set_leq_sort env sigma s1 s2 else Evd.set_eq_sort sigma s1 s2 in (sigma', metasubst, evarsubst) with e when Errors.noncritical e -> |