aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Interp.ml
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2019-07-08 10:48:24 +0200
committerGitHub <noreply@github.com>2019-07-08 10:48:24 +0200
commit96383f6dbccd4b280acad395b9a2683a645a9de3 (patch)
tree785fabd5bde83b9a690f9e46eb8e86e3448edfd3 /driver/Interp.ml
parent98858317be25deed815c7a8b5d4e9d6b512f5de5 (diff)
downloadcompcert-kvx-96383f6dbccd4b280acad395b9a2683a645a9de3.tar.gz
compcert-kvx-96383f6dbccd4b280acad395b9a2683a645a9de3.zip
Compatibility with OCaml 4.08 (#302)
* Do not use `Pervasives.xxx` qualified names Starting with OCaml 4.08, `Pervasives` is deprecated in favor of `Stdlib`, and uses of `Pervasives` cause fatal warnings. This commit uses unqualified names instead, as no ambiguity occurs. * Clarify "open" statements OCaml 4.08.0 has stricter warnings concerning open statements that shadow module names. Closes: #300
Diffstat (limited to 'driver/Interp.ml')
-rw-r--r--driver/Interp.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/driver/Interp.ml b/driver/Interp.ml
index 6760e76c..a6841460 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -15,7 +15,7 @@
open Format
open Camlcoq
open AST
-open Integers
+open !Integers
open Values
open Memory
open Globalenvs
@@ -145,7 +145,7 @@ let print_state p (prog, ge, s) =
let compare_mem m1 m2 =
(* assumes nextblocks were already compared equal *)
(* should permissions be taken into account? *)
- Pervasives.compare m1.Mem.mem_contents m2.Mem.mem_contents
+ compare m1.Mem.mem_contents m2.Mem.mem_contents
(* Comparing continuations *)