aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Interp.ml
diff options
context:
space:
mode:
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 *)