diff options
Diffstat (limited to 'kernel/nativevalues.ml')
| -rw-r--r-- | kernel/nativevalues.ml | 29 |
1 files changed, 1 insertions, 28 deletions
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 5712c997..8093df30 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -7,7 +7,7 @@ (************************************************************************) open Term open Names -open Errors +open CErrors open Util (** This module defines the representation of values internally used by @@ -78,8 +78,6 @@ let accumulate_code (k:accumulator) (x:t) = let rec accumulate (x:t) = accumulate_code (Obj.magic accumulate) x -let raccumulate = ref accumulate - let mk_accu_gen rcode (a:atom) = (* Format.eprintf "size rcode =%i\n" (Obj.size (Obj.magic rcode)); *) let r = Obj.new_block 0 3 in @@ -160,31 +158,6 @@ let is_accu x = let o = Obj.repr x in Obj.is_block o && Int.equal (Obj.tag o) accumulate_tag -(*let accumulate_fix_code (k:accumulator) (a:t) = - match atom_of_accu k with - | Afix(frec,_,rec_pos,_,_) -> - let nargs = accu_nargs k in - if nargs <> rec_pos || is_accu a then - accumulate_code k a - else - let r = ref frec in - for i = 0 to nargs - 1 do - r := !r (arg_of_accu k i) - done; - !r a - | _ -> assert false - - -let rec accumulate_fix (x:t) = - accumulate_fix_code (Obj.magic accumulate_fix) x - -let raccumulate_fix = ref accumulate_fix *) - -let is_atom_fix (a:atom) = - match a with - | Afix _ -> true - | _ -> false - let mk_fix_accu rec_pos pos types bodies = mk_accu_gen accumulate (Afix(types,bodies,rec_pos, pos)) |