From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 kernel/nativevalues.ml | 29 +----------------------------
 1 file changed, 1 insertion(+), 28 deletions(-)

(limited to 'kernel/nativevalues.ml')

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))
 
-- 
cgit v1.2.3