diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-01-29 09:10:29 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-01-29 09:10:29 +0000 |
commit | 056068abd228fefab4951a61700aa6d54fb88287 (patch) | |
tree | 6bf44526caf535e464e33999641b39032901fa67 /driver/Interp.ml | |
parent | 34d58b781afec8ecd4afdcf2ab83f1c972338ba9 (diff) | |
download | compcert-kvx-056068abd228fefab4951a61700aa6d54fb88287.tar.gz compcert-kvx-056068abd228fefab4951a61700aa6d54fb88287.zip |
Ported to Coq 8.4pl1. Merge of branches/coq-8.4.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'driver/Interp.ml')
-rw-r--r-- | driver/Interp.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/driver/Interp.ml b/driver/Interp.ml index f3d75ea3..9ea9d0c9 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -17,8 +17,6 @@ type caml_float = float open Format open Camlcoq open Datatypes -open BinPos -open BinInt open AST open Integers open Floats @@ -148,7 +146,7 @@ let compare_mem m1 m2 = (* should permissions be taken into account? *) (* Comparing continuations *) -let some_expr = Evar(Coq_xH, Tvoid) +let some_expr = Evar(P.one, Tvoid) let rank_cont = function | Kstop -> 0 @@ -258,7 +256,7 @@ let extract_string ge m id ofs = Some(Buffer.contents b) end else begin Buffer.add_char b c; - extract blk (coq_Zsucc ofs) + extract blk (Z.succ ofs) end | _ -> None in |