diff options
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 7eb8e803b3..a0023c11e6 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -24,6 +24,8 @@ open Type_errors module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration +exception NotConvertibleVect of int + let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y let conv_leq_vecti env v1 v2 = |