aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cbytecodes.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2015-10-12 10:51:08 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2015-10-12 10:52:01 +0200
commitc1ebc07204c65b4570333748b63a3ef60618b026 (patch)
tree9b930c31d03df7d80acc51972781fdeeba75c046 /kernel/cbytecodes.ml
parent303694c6436b36b114f4919ad7cacc9c053d11a3 (diff)
Gather VM tags in Cbytecodes.
Diffstat (limited to 'kernel/cbytecodes.ml')
-rw-r--r--kernel/cbytecodes.ml11
1 files changed, 7 insertions, 4 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 891d95378..448bf8544 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -17,13 +17,16 @@ open Term
type tag = int
-let id_tag = 0
-let iddef_tag = 1
-let ind_tag = 2
-let fix_tag = 3
+let accu_tag = 0
+
+let max_atom_tag = 1
+let proj_tag = 2
+let fix_app_tag = 3
let switch_tag = 4
let cofix_tag = 5
let cofix_evaluated_tag = 6
+
+
(* It would be great if OCaml exported this value,
So fixme if this happens in a new version of OCaml *)
let last_variant_tag = 245