diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-10-12 10:51:08 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-10-12 10:52:01 +0200 |
| commit | c1ebc07204c65b4570333748b63a3ef60618b026 (patch) | |
| tree | 9b930c31d03df7d80acc51972781fdeeba75c046 | |
| parent | 303694c6436b36b114f4919ad7cacc9c053d11a3 (diff) | |
Gather VM tags in Cbytecodes.
| -rw-r--r-- | kernel/cbytecodes.ml | 11 | ||||
| -rw-r--r-- | kernel/cbytecodes.mli | 10 | ||||
| -rw-r--r-- | kernel/vm.ml | 8 |
3 files changed, 13 insertions, 16 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 diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 8f594a45b..03d638305 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -13,13 +13,15 @@ open Term type tag = int -val id_tag : tag -val iddef_tag : tag -val ind_tag : tag -val fix_tag : tag +val accu_tag : tag + +val max_atom_tag : tag +val proj_tag : tag +val fix_app_tag : tag val switch_tag : tag val cofix_tag : tag val cofix_evaluated_tag : tag + val last_variant_tag : tag type structured_constant = diff --git a/kernel/vm.ml b/kernel/vm.ml index 29e2ee601..eacd803fd 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -19,14 +19,6 @@ external set_drawinstr : unit -> unit = "coq_set_drawinstr" external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure" external offset : Obj.t -> int = "coq_offset" -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 - (*******************************************) (* Initalization of the abstract machine ***) (*******************************************) |