diff options
Diffstat (limited to 'mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml')
| -rw-r--r-- | mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml | 15 |
1 files changed, 3 insertions, 12 deletions
diff --git a/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml b/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml index 0e5cf434..33c3c842 100644 --- a/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml +++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml @@ -53,14 +53,6 @@ let memo_int2pos: int -> int -> BinNums.positive Hashtbl.add t i pi; pi in find;; - -(* -let string_coq2caml: char list -> string - = fun l -> - let buf = Buffer.create (List.length l) in - List.iter (fun c -> Buffer.add_char buf c) l; - Buffer.contents buf;; -*) let new_exit_observer: (unit -> unit) -> (unit -> unit) ref = fun f -> @@ -123,8 +115,8 @@ let zTr: BinNums.coq_Z -> int let ten = BinNums.Zpos (BinNums.Coq_xO (BinNums.Coq_xI (BinNums.Coq_xO BinNums.Coq_xH))) let rec string_of_pos (p:BinNums.positive) (acc: pstring): pstring -= let (q,r) = BinInt.Z.pos_div_eucl p ten in - let acc0 = Concat (CamlStr (string_of_int (zTr r)), acc) in += let (q,r) = BinInt.Z.pos_div_eucl p ten in + let acc0 = Concat (CamlStr (string_of_int (zTr r)), acc) in match q with | BinNums.Z0 -> acc0 | BinNums.Zpos p0 -> string_of_pos p0 acc0 @@ -134,7 +126,7 @@ let rec string_of_pos (p:BinNums.positive) (acc: pstring): pstring let string_of_Z_debug: BinNums.coq_Z -> pstring = fun p -> CamlStr (string_of_int (zTr p)) *) - + let string_of_Z: BinNums.coq_Z -> pstring = function | BinNums.Z0 -> CamlStr "0" @@ -148,4 +140,3 @@ let timer ((f:'a -> 'b), (x:'a)) : 'b = let rt = (Unix.times()).Unix.tms_utime -. itime in Printf.printf "time = %f\n" rt; r - |