diff options
| author | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
| commit | c70412ec8b0bb34b7a5607c07d34607a147d834c (patch) | |
| tree | 0cc6cd76a8f70dfd2f5b55b0db96db4de2ff07a2 /kernel/nativeconv.ml | |
| parent | 720ee2730684cc289cef588482323d177e0bea59 (diff) | |
| parent | 191e253d1d1ebd6c76c63b3d83f4228e46196a6e (diff) | |
Merge PR #6914: Primitive integers
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
Diffstat (limited to 'kernel/nativeconv.ml')
| -rw-r--r-- | kernel/nativeconv.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index f5d7ab3c9d..baa290367f 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -34,6 +34,8 @@ let rec conv_val env pb lvl v1 v2 cu = conv_accu env pb lvl k1 k2 cu | Vconst i1, Vconst i2 -> if Int.equal i1 i2 then cu else raise NotConvertible + | Vint64 i1, Vint64 i2 -> + if Int64.equal i1 i2 then cu else raise NotConvertible | Vblock b1, Vblock b2 -> let n1 = block_size b1 in let n2 = block_size b2 in @@ -47,7 +49,7 @@ let rec conv_val env pb lvl v1 v2 cu = aux lvl max b1 b2 (i+1) cu in aux lvl (n1-1) b1 b2 0 cu - | Vaccu _, _ | Vconst _, _ | Vblock _, _ -> raise NotConvertible + | Vaccu _, _ | Vconst _, _ | Vint64 _, _ | Vblock _, _ -> raise NotConvertible and conv_accu env pb lvl k1 k2 cu = let n1 = accu_nargs k1 in |