aboutsummaryrefslogtreecommitdiff
path: root/kernel/primred.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/primred.ml')
-rw-r--r--kernel/primred.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/primred.ml b/kernel/primred.ml
index f158cfacea..17e5a89b74 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -12,7 +12,7 @@ type _ action_kind =
type exn += IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn
let check_same_types typ c1 c2 =
- if not (Constant.equal c1 c2)
+ if not (Constant.CanOrd.equal c1 c2)
then raise (IncompatibleDeclarations (IncompatTypes typ, c1, c2))
let check_same_inds ind i1 i2 =