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

9 files changed, 11 insertions, 12 deletions

diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index 46d5c3f1..902724e0 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -106,7 +106,7 @@ let flatten_blocks blks =
   let cmp_minpc (mpc1, _) (mpc2, _) =
     if mpc1 = mpc2 then 0 else if mpc1 > mpc2 then -1 else 1
   in
-    List.flatten (List.map Pervasives.snd (List.sort cmp_minpc blks))
+    List.flatten (List.map snd (List.sort cmp_minpc blks))
 
 (* Build the enumeration *)
 
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index dd428808..155f5e55 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -13,7 +13,6 @@
 
 open AST
 open Camlcoq
-open DwarfPrinter
 open PrintAsmaux
 open Printf
 open Sections
@@ -177,7 +176,7 @@ module Printer(Target:TARGET) =
         let address = Target.address
       end
 
-    module DebugPrinter = DwarfPrinter (DwarfTarget)
+    module DebugPrinter = DwarfPrinter.DwarfPrinter (DwarfTarget)
   end
 
 let print_program oc p =
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index f68c1267..8c255a65 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -16,7 +16,7 @@
 (** Pretty-printer for Cminor *)
 
 open Format
-open Camlcoq
+open !Camlcoq
 open Integers
 open AST
 open PrintAST
diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml
index d0557073..1c449e74 100644
--- a/backend/PrintLTL.ml
+++ b/backend/PrintLTL.ml
@@ -112,7 +112,7 @@ let print_function pp id f =
   fprintf pp "%s() {\n" (extern_atom id);
   let instrs =
     List.sort
-      (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
+      (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
       (List.rev_map
         (fun (pc, i) -> (P.to_int pc, i))
         (PTree.elements f.fn_code)) in
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
index ba336b0a..841540b6 100644
--- a/backend/PrintRTL.ml
+++ b/backend/PrintRTL.ml
@@ -93,7 +93,7 @@ let print_function pp id f =
   fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params;
   let instrs =
     List.sort
-      (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
+      (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
       (List.rev_map
         (fun (pc, i) -> (P.to_int pc, i))
         (PTree.elements f.fn_code)) in
diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml
index cc1f7d49..6432682a 100644
--- a/backend/PrintXTL.ml
+++ b/backend/PrintXTL.ml
@@ -138,7 +138,7 @@ let print_function pp ?alloc ?live f =
   fprintf pp "f() {\n";
   let instrs =
     List.sort
-      (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
+      (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
       (List.map
         (fun (pc, i) -> (P.to_int pc, i))
         (PTree.elements f.fn_code)) in
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 5ff58780..7a2f4828 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -29,7 +29,7 @@ let no_loc = ("", -1)
 
 module Ident = struct
   type t = ident
-  let compare id1 id2 = Pervasives.compare id1.stamp id2.stamp
+  let compare id1 id2 = compare id1.stamp id2.stamp
 end
 
 module IdentSet = Set.Make(Ident)
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index bbfcf311..9a24041b 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -268,7 +268,7 @@ module DwarfPrinter(Target: DWARF_TARGET):
     (* Print the debug_abbrev section using the previous computed abbreviations*)
     let print_abbrev oc =
       let abbrevs = Hashtbl.fold (fun s i acc -> (s,i)::acc) abbrev_mapping [] in
-      let abbrevs = List.sort (fun (_,a) (_,b) -> Pervasives.compare a b) abbrevs in
+      let abbrevs = List.sort (fun (_,a) (_,b) -> compare a b) abbrevs in
       section oc Section_debug_abbrev;
       print_label oc !abbrev_start_addr;
       List.iter (fun (s,id) ->
@@ -685,7 +685,7 @@ module DwarfPrinter(Target: DWARF_TARGET):
       print_label oc line_start;
       list_opt s (fun () ->
         section oc Section_debug_str;
-        let s = List.sort (fun (a,_) (b,_) -> Pervasives.compare a b) s in
+        let s = List.sort (fun (a,_) (b,_) -> compare a b) s in
         List.iter (fun (id,s) ->
           print_label oc (loc_to_label id);
           fprintf oc "	.asciz		%S\n" s) s)
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 *)