summaryrefslogtreecommitdiff
path: root/kernel/vconv.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-07-15 13:15:50 +0200
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-07-15 13:15:50 +0200
commite347929583f820a2cc0296597b6382309e930989 (patch)
treecdc3f18fc5c66a9d3d7cc8404c6a295169e41fcc /kernel/vconv.ml
parentc01be74d81a5466c58f8dc6c568db286b0979997 (diff)
parent0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff)
Merge tag 'upstream/8.5_beta2+dfsg' into test
Upstream version 8.5~beta2+dfsg
Diffstat (limited to 'kernel/vconv.ml')
-rw-r--r--kernel/vconv.ml5
1 files changed, 2 insertions, 3 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 80b15f8b..1c31cc04 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -42,8 +42,6 @@ let conv_vect fconv vect1 vect2 cu =
let infos = ref (create_clos_infos betaiotazeta Environ.empty_env)
-let eq_table_key = Names.eq_table_key eq_constant
-
let rec conv_val env pb k v1 v2 cu =
if v1 == v2 then cu
else conv_whd env pb k (whd_val v1) (whd_val v2) cu
@@ -66,8 +64,9 @@ and conv_whd env pb k whd1 whd2 cu =
| Vconstr_const i1, Vconstr_const i2 ->
if Int.equal i1 i2 then cu else raise NotConvertible
| Vconstr_block b1, Vconstr_block b2 ->
+ let tag1 = btag b1 and tag2 = btag b2 in
let sz = bsize b1 in
- if Int.equal (btag b1) (btag b2) && Int.equal sz (bsize b2) then
+ if Int.equal tag1 tag2 && Int.equal sz (bsize b2) then
let rcu = ref cu in
for i = 0 to sz - 1 do
rcu := conv_val env CONV k (bfield b1 i) (bfield b2 i) !rcu