aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/typeops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/typeops.ml')
-rw-r--r--checker/typeops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/typeops.ml b/checker/typeops.ml
index b904e0b68..98f071fa0 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -256,7 +256,7 @@ let refresh_arity env ar =
match hd with
Sort (Type u) when not (is_univ_variable u) ->
let u' = fresh_local_univ() in
- let env' = add_constraints (enforce_geq u' u empty_constraint) env in
+ let env' = add_constraints (enforce_leq u u' empty_constraint) env in
env', mkArity (ctxt,Type u')
| _ -> env, ar