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

3 files changed, 12 insertions, 13 deletions

diff --git a/driver/Compiler.v b/driver/Compiler.v
index ed27f38..9db7f42 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -217,18 +217,18 @@ Proof.
   repeat rewrite compose_print_identity in H.
   simpl in H.
   set (p1 := Tailcall.transf_program p) in *.
-  destruct (Inlining.transf_program p1) as [p11|]_eqn; simpl in H; try discriminate.
+  destruct (Inlining.transf_program p1) as [p11|] eqn:?; simpl in H; try discriminate.
   set (p12 := Renumber.transf_program p11) in *.
   set (p2 := Constprop.transf_program p12) in *.
   set (p21 := Renumber.transf_program p2) in *.
-  destruct (CSE.transf_program p21) as [p3|]_eqn; simpl in H; try discriminate.
-  destruct (Allocation.transf_program p3) as [p4|]_eqn; simpl in H; try discriminate.
+  destruct (CSE.transf_program p21) as [p3|] eqn:?; simpl in H; try discriminate.
+  destruct (Allocation.transf_program p3) as [p4|] eqn:?; simpl in H; try discriminate.
   set (p5 := Tunneling.tunnel_program p4) in *.
-  destruct (Linearize.transf_program p5) as [p6|]_eqn; simpl in H; try discriminate.
+  destruct (Linearize.transf_program p5) as [p6|] eqn:?; simpl in H; try discriminate.
   set (p7 := CleanupLabels.transf_program p6) in *.
   set (p8 := Reload.transf_program p7) in *.
   set (p9 := RRE.transf_program p8) in *.
-  destruct (Stacking.transf_program p9) as [p10|]_eqn; simpl in H; try discriminate.
+  destruct (Stacking.transf_program p9) as [p10|] eqn:?; simpl in H; try discriminate.
 
   assert(TY1: LTLtyping.wt_program p5).
     eapply Tunnelingtyping.program_typing_preserved. 
@@ -274,7 +274,7 @@ Proof.
   repeat rewrite compose_print_identity in H.
   simpl in H. 
   set (p1 := Selection.sel_program p) in *.
-  destruct (RTLgen.transl_program p1) as [p2|]_eqn; simpl in H; try discriminate.
+  destruct (RTLgen.transl_program p1) as [p2|] eqn:?; simpl in H; try discriminate.
   eapply compose_forward_simulation. apply Selectionproof.transf_program_correct.
   eapply compose_forward_simulation. apply RTLgenproof.transf_program_correct. eassumption.
   exact (fst (transf_rtl_program_correct _ _ H)).
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 85f6079..6c00cb7 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -11,6 +11,7 @@
 (* *********************************************************************)
 
 open Printf
+open Camlcoq
 open Clflags
 
 (* Location of the compatibility library *)
@@ -37,9 +38,9 @@ let safe_remove file =
 
 let print_error oc msg =
   let print_one_error = function
-  | Errors.MSG s -> output_string oc (Camlcoq.camlstring_of_coqstring s)
-  | Errors.CTX i -> output_string oc (Camlcoq.extern_atom i)
-  | Errors.POS i -> fprintf oc "%ld" (Camlcoq.camlint_of_positive i)
+  | Errors.MSG s -> output_string oc (camlstring_of_coqstring s)
+  | Errors.CTX i -> output_string oc (extern_atom i)
+  | Errors.POS i -> fprintf oc "%ld" (P.to_int32 i)
   in
     List.iter print_one_error msg;
     output_char oc '\n'
diff --git a/driver/Interp.ml b/driver/Interp.ml
index f3d75ea..9ea9d0c 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