diff options
Diffstat (limited to 'kernel/vm.ml')
| -rw-r--r-- | kernel/vm.ml | 8 |
1 files changed, 0 insertions, 8 deletions
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 ***) (*******************************************) |