From 8c24fc1ba49a1623dbecbea82c9fef238f17c4ee Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 2 Oct 2012 15:58:10 +0000 Subject: Remove some dead code in the vm Apparently Cysmtable.set_global_boxed is unused, and removing it allows to get rid of a bunch of C code concerning "boxed" things (including ACCUMULATECOND instruction). Still TODO: Csymtable.set_transparent_const and Csymtable.set_opaque_const appear to be no-ops. Should we remove them ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15845 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/vm.ml | 8 -------- 1 file changed, 8 deletions(-) (limited to 'kernel/vm.ml') diff --git a/kernel/vm.ml b/kernel/vm.ml index 656e555fc..d4a86cb49 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -42,7 +42,6 @@ let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0) external mkAccuCode : int -> tcode = "coq_makeaccu" external mkPopStopCode : int -> tcode = "coq_pushpop" -external mkAccuCond : int -> tcode = "coq_accucond" external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode" external int_tcode : tcode -> int -> int = "coq_int_tcode" @@ -315,17 +314,10 @@ let val_of_idkey key = v let val_of_rel k = val_of_idkey (RelKey k) -let val_of_rel_def k v = val_of_atom(Aiddef(RelKey k, v)) let val_of_named id = val_of_idkey (VarKey id) -let val_of_named_def id v = val_of_atom(Aiddef(VarKey id, v)) let val_of_constant c = val_of_idkey (ConstKey c) -let val_of_constant_def n c v = - let res = Obj.new_block accu_tag 2 in - Obj.set_field res 0 (Obj.repr (mkAccuCond n)); - Obj.set_field res 1 (Obj.repr (Aiddef(ConstKey c, v))); - val_of_obj res external val_of_annot_switch : annot_switch -> values = "%identity" -- cgit v1.2.3