aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/glob_ops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index ba193da60..988bdae03 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -112,7 +112,7 @@ let fix_kind_eq f k1 k2 = match k1, k2 with
let eq (i1, o1) (i2, o2) =
Option.equal Int.equal i1 i2 && fix_recursion_order_eq f o1 o2
in
- Int.equal i1 i2 && Array.equal eq a1 a1
+ Int.equal i1 i2 && Array.equal eq a1 a2
| GCoFix i1, GCoFix i2 -> Int.equal i1 i2
| (GFix _ | GCoFix _), _ -> false