aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-02-21 15:11:30 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-02-26 14:53:08 +0100
commit969f56084f2c9eac670e47852518a3ca11fb0174 (patch)
treed5022bdb00088f5f31ae901c6e6875e25ce8bf97
parent83ee68ba8beda04343514d9e5905ea062cbeada0 (diff)
fix checker w.r.t. Dyn.t validation
discrepancy introduced in commit 400327165edcba667ebb70ebb89052455656b719
-rw-r--r--checker/validate.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/validate.ml b/checker/validate.ml
index 6a1a26c31..3f9aabdfa 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -60,7 +60,7 @@ let val_dyn ctx o =
let fail () = fail ctx o "expected a Dyn.t" in
if not (Obj.is_block o) then fail ()
else if not (Obj.size o = 2) then fail ()
- else if not (Obj.tag (Obj.field o 0) = Obj.string_tag) then fail ()
+ else if not (Obj.tag (Obj.field o 0) = Obj.int_tag) then fail ()
else ()
open Values