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

19 files changed, 104 insertions, 120 deletions

diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll
index eac48e0..4083c95 100644
--- a/backend/CMlexer.mll
+++ b/backend/CMlexer.mll
@@ -14,6 +14,7 @@
 (* *********************************************************************)
 
 {
+open BinNums
 open Camlcoq
 open CMparser
 exception Error of string
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index ff77c03..eb3b9ab 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -19,8 +19,7 @@
 %{
 open Datatypes
 open Camlcoq
-open BinPos
-open BinInt
+open BinNums
 open Integers
 open AST
 open Cminor
@@ -45,16 +44,16 @@ let mkef sg toks =
       EF_vstore c
   | [EFT_tok "volatile"; EFT_tok "load"; EFT_chunk c; 
      EFT_tok "global"; EFT_string s; EFT_int n] ->
-      EF_vload_global(c, intern_string s, z_of_camlint n)
+      EF_vload_global(c, intern_string s, coqint_of_camlint n)
   | [EFT_tok "volatile"; EFT_tok "store"; EFT_chunk c; 
      EFT_tok "global"; EFT_string s; EFT_int n] ->
-      EF_vstore_global(c, intern_string s, z_of_camlint n)
+      EF_vstore_global(c, intern_string s, coqint_of_camlint n)
   | [EFT_tok "malloc"] ->
       EF_malloc
   | [EFT_tok "free"] ->
       EF_free
   | [EFT_tok "memcpy"; EFT_tok "size"; EFT_int sz; EFT_tok "align"; EFT_int al] ->
-      EF_memcpy(z_of_camlint sz, z_of_camlint al)
+      EF_memcpy(Z.of_sint32 sz, Z.of_sint32 al)
   | [EFT_tok "annot"; EFT_string txt] ->
       EF_annot(intern_string txt, sg.sig_args)
   | [EFT_tok "annot_val"; EFT_string txt] ->
@@ -183,7 +182,7 @@ let mkwhile expr body =
 let intconst n =
   Rconst(Ointconst(coqint_of_camlint n))
 
-let exitnum n = nat_of_camlint n
+let exitnum n = Nat.of_int32 n
 
 let mkswitch expr (cases, dfl) =
   convert_accu := [];
@@ -211,25 +210,25 @@ let mkswitch expr (cases, dfl) =
 ***)
 
 let mkmatch_aux expr cases =
-  let ncases = Int32.of_int (List.length cases) in
+  let ncases = List.length cases in
   let rec mktable n = function
     | [] -> assert false
     | [key, action] -> []
     | (key, action) :: rem ->
-        (coqint_of_camlint key, nat_of_camlint n)
-        :: mktable (Int32.succ n) rem in
+        (coqint_of_camlint key, Nat.of_int n)
+        :: mktable (n + 1) rem in
   let sw =
-    Sswitch(expr, mktable 0l cases, nat_of_camlint (Int32.pred ncases)) in
+    Sswitch(expr, mktable 0 cases, Nat.of_int (ncases - 1)) in
   let rec mkblocks body n = function
     | [] -> assert false
     | [key, action] ->
         Sblock(Sseq(body, action))
     | (key, action) :: rem ->
         mkblocks
-          (Sblock(Sseq(body, Sseq(action, Sexit (nat_of_camlint n)))))
-          (Int32.pred n)
+          (Sblock(Sseq(body, Sseq(action, Sexit (Nat.of_int n)))))
+          (n - 1)
           rem in
-  mkblocks (Sblock sw) (Int32.pred ncases) cases
+  mkblocks (Sblock sw) (ncases - 1) cases
 
 let mkmatch expr cases =
   convert_accu := [];
@@ -377,7 +376,7 @@ global_declaration:
       { $1 }
   | VAR STRINGLIT LBRACKET INTLIT RBRACKET  /* old style */
       { (intern_string $2,
-         Gvar{gvar_info = (); gvar_init = [Init_space(z_of_camlint $4)];
+         Gvar{gvar_info = (); gvar_init = [Init_space(Z.of_sint32 $4)];
               gvar_readonly = false; gvar_volatile = false}) }
   | VAR STRINGLIT is_readonly is_volatile LBRACE init_data_list RBRACE
        { (intern_string $2,
@@ -413,7 +412,7 @@ init_data:
    | FLOAT64 FLOATLIT                            { Init_float64 (coqfloat_of_camlfloat $2) }
    | FLOAT FLOATLIT                              { Init_float64 (coqfloat_of_camlfloat $2) }
    | FLOATLIT                                    { Init_float64 (coqfloat_of_camlfloat $1) }
-   | LBRACKET INTLIT RBRACKET                    { Init_space (z_of_camlint $2) }
+   | LBRACKET INTLIT RBRACKET                    { Init_space (Z.of_sint32 $2) }
    | INTLIT LPAREN STRINGLIT RPAREN              { Init_addrof (intern_string $3, coqint_of_camlint $1) }
  ;
  
@@ -462,7 +461,7 @@ parameter_list:
 
 stack_declaration:
     /* empty */                                 { Z0 }
-  | STACK INTLIT SEMICOLON                      { z_of_camlint $2 }
+  | STACK INTLIT SEMICOLON                      { Z.of_sint32 $2 }
 ;
 
 var_declarations:
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
index 408e9ec..39e8c51 100644
--- a/backend/CMtypecheck.ml
+++ b/backend/CMtypecheck.ml
@@ -64,7 +64,7 @@ let type_var env id =
     raise (Error (sprintf "Unbound variable %s\n" (extern_atom id)))
 
 let type_letvar env n =
-  let n = camlint_of_nat n in
+  let n = Nat.to_int n in
   try
     List.nth env n
   with Not_found ->
@@ -303,8 +303,8 @@ let rec type_stmt env blk ret s =
   | Sblock s1 ->
       type_stmt env (blk + 1) ret s1
   | Sexit n ->
-      if camlint_of_nat n >= blk then
-        raise (Error (sprintf "Bad exit(%d)\n" (camlint_of_nat n)))
+      if Nat.to_int n >= blk then
+        raise (Error (sprintf "Bad exit(%d)\n" (Nat.to_int n)))
   | Sswitch(e, cases, deflt) ->
       unify (type_expr env [] e) tint
   | Sreturn None ->
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 5569123..44d23c8 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -94,7 +94,7 @@ Lemma wf_valnum_reg:
   wf_numbering n' /\ Plt v n'.(num_next) /\ Ple n.(num_next) n'.(num_next).
 Proof.
   intros until v. unfold valnum_reg. intros WF VREG. inversion WF.
-  destruct ((num_reg n)!r) as [v'|]_eqn.
+  destruct ((num_reg n)!r) as [v'|] eqn:?.
 (* found *)
   inv VREG. split. auto. split. eauto. apply Ple_refl.
 (* not found *)
@@ -174,7 +174,7 @@ Lemma wf_forget_reg:
   In r (PMap.get v (forget_reg n rd)) -> r <> rd /\ PTree.get r n.(num_reg) = Some v.
 Proof.
   unfold forget_reg; intros. inversion H. 
-  destruct ((num_reg n)!rd) as [vd|]_eqn. 
+  destruct ((num_reg n)!rd) as [vd|] eqn:?. 
   rewrite PMap.gsspec in H0. destruct (peq v vd). 
   subst vd. rewrite in_remove in H0. destruct H0. split. auto. eauto. 
   split; eauto. exploit VAL; eauto. congruence. 
@@ -201,7 +201,7 @@ Lemma wf_add_rhs:
   wf_numbering (add_rhs n rd rh).
 Proof.
   intros. inversion H. unfold add_rhs. 
-  destruct (find_valnum_rhs rh n.(num_eqs)) as [vres|]_eqn.
+  destruct (find_valnum_rhs rh n.(num_eqs)) as [vres|] eqn:?.
 (* found *)
   exploit find_valnum_rhs_correct; eauto. intros IN. 
   split; simpl; intros. 
@@ -226,16 +226,16 @@ Lemma wf_add_op:
   wf_numbering n ->
   wf_numbering (add_op n rd op rs).
 Proof.
-  intros. unfold add_op. destruct (is_move_operation op rs) as [r|]_eqn.
+  intros. unfold add_op. destruct (is_move_operation op rs) as [r|] eqn:?.
 (* move *)
-  destruct (valnum_reg n r) as [n' v]_eqn.
+  destruct (valnum_reg n r) as [n' v] eqn:?.
   exploit wf_valnum_reg; eauto. intros [A [B C]]. inversion A.
   constructor; simpl; intros.
   eauto.
   rewrite PTree.gsspec in H0. destruct (peq r0 rd). inv H0. auto. eauto.
   eapply wf_update_reg; eauto. 
 (* not a move *)
-  destruct (valnum_regs n rs) as [n' vs]_eqn.
+  destruct (valnum_regs n rs) as [n' vs] eqn:?.
   exploit wf_valnum_regs; eauto. intros [A [B C]].
   eapply wf_add_rhs; eauto.
 Qed.
@@ -270,7 +270,7 @@ Remark kill_eqs_in:
 Proof.
   induction eqs; simpl; intros. 
   tauto.
-  destruct (pred (snd a)) as []_eqn. 
+  destruct (pred (snd a)) eqn:?. 
   exploit IHeqs; eauto. tauto. 
   simpl in H; destruct H. subst a. auto. exploit IHeqs; eauto. tauto. 
 Qed.
@@ -289,7 +289,7 @@ Lemma wf_add_store:
   wf_numbering n -> wf_numbering (add_store n chunk addr rargs rsrc).
 Proof.
   intros. unfold add_store. 
-  destruct (valnum_regs n rargs) as [n1 vargs]_eqn.
+  destruct (valnum_regs n rargs) as [n1 vargs] eqn:?.
   exploit wf_valnum_regs; eauto. intros [A [B C]].
   assert (wf_numbering (kill_equations (filter_after_store chunk addr vargs) n1)).
     apply wf_kill_equations. auto.
@@ -664,7 +664,7 @@ Lemma add_store_satisfiable:
   numbering_satisfiable ge sp rs m' (add_store n chunk addr args src).
 Proof.
   intros. unfold add_store. destruct H0 as [valu A].
-  destruct (valnum_regs n args) as [n1 vargs]_eqn.
+  destruct (valnum_regs n args) as [n1 vargs] eqn:?.
   exploit valnum_regs_holds; eauto. intros [valu' [B [C D]]].
   exploit wf_valnum_regs; eauto. intros [U [V W]].
   set (n2 := kill_equations (filter_after_store chunk addr vargs) n1).
@@ -704,7 +704,7 @@ Lemma reg_valnum_correct:
   forall n v r, wf_numbering n -> reg_valnum n v = Some r -> n.(num_reg)!r = Some v.
 Proof.
   unfold reg_valnum; intros. inv H. 
-  destruct ((num_val n)#v) as [| r1 rl]_eqn; inv H0. 
+  destruct ((num_val n)#v) as [| r1 rl] eqn:?; inv H0. 
   eapply VAL. rewrite Heql. auto with coqlib.
 Qed.
 
@@ -755,8 +755,8 @@ Lemma regs_valnums_correct:
 Proof.
   induction vl; simpl; intros.
   inv H. auto.
-  destruct (reg_valnum n a) as [r1|]_eqn; try discriminate.
-  destruct (regs_valnums n vl) as [rx|]_eqn; try discriminate.
+  destruct (reg_valnum n a) as [r1|] eqn:?; try discriminate.
+  destruct (regs_valnums n vl) as [rx|] eqn:?; try discriminate.
   inv H. simpl; decEq; auto. 
   eapply (proj2 n_holds); eauto. eapply reg_valnum_correct; eauto.
 Qed.
@@ -770,13 +770,13 @@ Proof.
   induction niter; simpl; intros.
   discriminate.
   destruct (f (fun v : valnum => find_valnum_num v (num_eqs n)) op args)
-           as [[op1 args1] | ]_eqn.
+           as [[op1 args1] | ] eqn:?.
   assert (sem op1 (map valu args1) = Some res).
     rewrite <- H0. eapply f_sound; eauto.
     simpl; intros. apply (proj1 n_holds). eapply find_valnum_num_correct; eauto. 
-  destruct (reduce_rec A f n niter op1 args1) as [[op2 rl2] | ]_eqn.
+  destruct (reduce_rec A f n niter op1 args1) as [[op2 rl2] | ] eqn:?.
   inv H. eapply IHniter; eauto.
-  destruct (regs_valnums n args1) as [rl|]_eqn.
+  destruct (regs_valnums n args1) as [rl|] eqn:?.
   inv H. erewrite regs_valnums_correct; eauto.
   discriminate.
   discriminate.
@@ -790,7 +790,7 @@ Lemma reduce_sound:
   sem op' rs##rl' = Some res.
 Proof.
   unfold reduce; intros. 
-  destruct (reduce_rec A f n 4%nat op vl) as [[op1 rl1] | ]_eqn; inv H.
+  destruct (reduce_rec A f n 4%nat op vl) as [[op1 rl1] | ] eqn:?; inv H.
   eapply reduce_rec_sound; eauto. congruence.
   auto.
 Qed.
@@ -973,21 +973,21 @@ Proof.
 
   (* Iop *)
   exists (State s' (transf_function' f approx) sp pc' (rs#res <- v) m); split.
-  destruct (is_trivial_op op) as []_eqn.
+  destruct (is_trivial_op op) eqn:?.
   eapply exec_Iop'; eauto.
   rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
-  destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn.
+  destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
   assert (wf_numbering approx!!pc). eapply wf_analyze; eauto.
   destruct SAT as [valu1 NH1].
   exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. 
   assert (wf_numbering n1). eapply wf_valnum_regs; eauto. 
-  destruct (find_rhs n1 (Op op vl)) as [r|]_eqn.
+  destruct (find_rhs n1 (Op op vl)) as [r|] eqn:?.
   (* replaced by move *)
   assert (EV: rhs_evals_to ge sp valu2 (Op op vl) m rs#r). eapply find_rhs_correct; eauto.
   assert (RES: rs#r = v). red in EV. congruence.
   eapply exec_Iop'; eauto. simpl. congruence. 
   (* possibly simplified *)
-  destruct (reduce operation combine_op n1 op args vl) as [op' args']_eqn.
+  destruct (reduce operation combine_op n1 op args vl) as [op' args'] eqn:?.
   assert (RES: eval_operation ge sp op' rs##args' m = Some v).
     eapply reduce_sound with (sem := fun op vl => eval_operation ge sp op vl m); eauto. 
     intros; eapply combine_op_sound; eauto.
@@ -1007,18 +1007,18 @@ Proof.
 
   (* Iload *)
   exists (State s' (transf_function' f approx) sp pc' (rs#dst <- v) m); split.
-  destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn.
+  destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
   assert (wf_numbering approx!!pc). eapply wf_analyze; eauto.
   destruct SAT as [valu1 NH1].
   exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. 
   assert (wf_numbering n1). eapply wf_valnum_regs; eauto. 
-  destruct (find_rhs n1 (Load chunk addr vl)) as [r|]_eqn.
+  destruct (find_rhs n1 (Load chunk addr vl)) as [r|] eqn:?.
   (* replaced by move *)
   assert (EV: rhs_evals_to ge sp valu2 (Load chunk addr vl) m rs#r). eapply find_rhs_correct; eauto.
   assert (RES: rs#r = v). red in EV. destruct EV as [a' [EQ1 EQ2]]. congruence.
   eapply exec_Iop'; eauto. simpl. congruence. 
   (* possibly simplified *)
-  destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args']_eqn.
+  destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args'] eqn:?.
   assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a).
     eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. 
     intros; eapply combine_addr_sound; eauto.
@@ -1035,12 +1035,12 @@ Proof.
 
   (* Istore *)
   exists (State s' (transf_function' f approx) sp pc' rs m'); split.
-  destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn.
+  destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
   assert (wf_numbering approx!!pc). eapply wf_analyze; eauto.
   destruct SAT as [valu1 NH1].
   exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. 
   assert (wf_numbering n1). eapply wf_valnum_regs; eauto. 
-  destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args']_eqn.
+  destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args'] eqn:?.
   assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a).
     eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. 
     intros; eapply combine_addr_sound; eauto.
@@ -1093,12 +1093,12 @@ Proof.
   eapply kill_loads_satisfiable; eauto. 
 
   (* Icond *)
-  destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn.
+  destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
   assert (wf_numbering approx!!pc). eapply wf_analyze; eauto.
   elim SAT; intros valu1 NH1.
   exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. 
   assert (wf_numbering n1). eapply wf_valnum_regs; eauto. 
-  destruct (reduce condition combine_cond n1 cond args vl) as [cond' args']_eqn.
+  destruct (reduce condition combine_cond n1 cond args vl) as [cond' args'] eqn:?.
   assert (RES: eval_condition cond' rs##args' m = Some b).
     eapply reduce_sound with (sem := fun cond vl => eval_condition cond vl m); eauto. 
     intros; eapply combine_cond_sound; eauto.
@@ -1124,8 +1124,8 @@ Proof.
 
   (* internal function *)
   monadInv H7. unfold transf_function in EQ. 
-  destruct (type_function f) as [tyenv|]_eqn; try discriminate.
-  destruct (analyze f) as [approx|]_eqn; inv EQ. 
+  destruct (type_function f) as [tyenv|] eqn:?; try discriminate.
+  destruct (analyze f) as [approx|] eqn:?; inv EQ. 
   assert (WTF: wt_function f tyenv). apply type_function_correct; auto.
   econstructor; split.
   eapply exec_function_internal; eauto. 
diff --git a/backend/Coloringaux.ml b/backend/Coloringaux.ml
index 2fce25e..ddd3094 100644
--- a/backend/Coloringaux.ml
+++ b/backend/Coloringaux.ml
@@ -12,8 +12,6 @@
 
 open Camlcoq
 open Datatypes
-open BinPos
-open BinInt
 open AST
 open Maps
 open Registers
@@ -766,8 +764,8 @@ let rec reuse_slot conflicts n mvlist =
 let find_slot conflicts typ =
   let rec find curr =
     let l = S(Local(curr, typ)) in
-    if Locset.mem l conflicts then find (coq_Zsucc curr) else l
-  in find Z0
+    if Locset.mem l conflicts then find (Z.succ curr) else l
+  in find Z.zero
 
 let assign_color n =
   let conflicts = ref Locset.empty in
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 1b90666..cd757cd 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -199,9 +199,9 @@ Lemma eval_static_load_sound:
   val_match_approx ge sp (eval_static_load gapp chunk addr) v.
 Proof.
   intros. unfold eval_static_load. destruct addr; simpl; auto. 
-  destruct (gapp!i) as [il|]_eqn; auto.
+  destruct (gapp!i) as [il|] eqn:?; auto.
   red in H1. subst vaddr. unfold symbol_address in H. 
-  destruct (Genv.find_symbol ge i) as [b'|]_eqn; simpl in H; try discriminate.
+  destruct (Genv.find_symbol ge i) as [b'|] eqn:?; simpl in H; try discriminate.
   exploit H0; eauto. intros [A [B C]]. 
   eapply eval_load_init_sound; eauto. 
   red; auto. 
@@ -290,7 +290,7 @@ Proof.
                \/ id0 <> id /\ ga!id0 = Some il).
   destruct gd.
   rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id); [discriminate|auto].
-  destruct (gvar_readonly v && negb (gvar_volatile v)) as []_eqn.
+  destruct (gvar_readonly v && negb (gvar_volatile v)) eqn:?.
   rewrite PTree.gsspec in H0. destruct (peq id0 id).
   inv H0. left. split; auto. 
   destruct v; simpl in *. 
@@ -455,10 +455,10 @@ Lemma match_successor_rec:
 Proof.
   induction n; simpl; intros.
   apply match_pc_base.
-  destruct (fn_code f)!pc as [i|]_eqn; try apply match_pc_base.
+  destruct (fn_code f)!pc as [i|] eqn:?; try apply match_pc_base.
   destruct i; try apply match_pc_base.
   eapply match_pc_nop; eauto. 
-  destruct (eval_static_condition c (approx_regs app l)) as [b|]_eqn.
+  destruct (eval_static_condition c (approx_regs app l)) as [b|] eqn:?.
   eapply match_pc_cond; eauto.
   apply match_pc_base.
 Qed.
@@ -607,7 +607,7 @@ Proof.
   assert (MATCH'': regs_match_approx sp (analyze gapp f) # pc' rs # res <- v).
     eapply analyze_correct_1 with (pc := pc); eauto. simpl; auto.
     unfold transfer; rewrite H. auto.  
-  destruct (const_for_result a) as [cop|]_eqn; intros.
+  destruct (const_for_result a) as [cop|] eqn:?; intros.
   (* constant is propagated *)
   left; econstructor; econstructor; split.
   eapply exec_Iop; eauto. 
@@ -640,7 +640,7 @@ Proof.
     eapply approx_regs_val_list; eauto.
   assert (VM2: val_match_approx ge sp ap2 v).
     eapply eval_static_load_sound; eauto.
-  destruct (const_for_result ap2) as [cop|]_eqn; intros.
+  destruct (const_for_result ap2) as [cop|] eqn:?; intros.
   (* constant-propagated *)
   left; econstructor; econstructor; split.
   eapply exec_Iop; eauto. eapply const_for_result_correct; eauto.
@@ -708,7 +708,7 @@ Proof.
   (* Ibuiltin *)
   rename pc'0 into pc.
 Opaque builtin_strength_reduction.
-  destruct (builtin_strength_reduction ef args (approx_regs (analyze gapp f)#pc args)) as [ef' args']_eqn.
+  destruct (builtin_strength_reduction ef args (approx_regs (analyze gapp f)#pc args)) as [ef' args'] eqn:?.
   generalize (builtin_strength_reduction_correct ge sp (analyze gapp f)!!pc rs
                   MATCH2 ef args (approx_regs (analyze gapp f) # pc args) _ _ _ _ (refl_equal _) H0).
   rewrite Heqp. intros P.
@@ -732,7 +732,7 @@ Opaque builtin_strength_reduction.
   destruct (cond_strength_reduction cond args (approx_regs (analyze gapp f) # pc args)) as [cond' args'].
   intros EV1 TCODE.
   left; exists O; exists (State s' (transf_function gapp f) sp (if b then ifso else ifnot) rs' m'); split. 
-  destruct (eval_static_condition cond (approx_regs (analyze gapp f) # pc args)) as []_eqn.
+  destruct (eval_static_condition cond (approx_regs (analyze gapp f) # pc args)) eqn:?.
   assert (eval_condition cond rs ## args m = Some b0).
     eapply eval_static_condition_correct; eauto. eapply approx_regs_val_list; eauto.
   assert (b = b0) by congruence. subst b0.
@@ -758,7 +758,7 @@ Opaque builtin_strength_reduction.
   rename pc'0 into pc.
   assert (A: (fn_code (transf_function gapp f))!pc = Some(Ijumptable arg tbl)
              \/ (fn_code (transf_function gapp f))!pc = Some(Inop pc')).
-  TransfInstr. destruct (approx_reg (analyze gapp f) # pc arg) as []_eqn; auto.
+  TransfInstr. destruct (approx_reg (analyze gapp f) # pc arg) eqn:?; auto.
   generalize (MATCH2 arg). unfold approx_reg in Heqt. rewrite Heqt. rewrite H0. 
   simpl. intro EQ; inv EQ. rewrite H1. auto.
   assert (B: rs'#arg = Vint n).
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index 8de8487..9536141 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -306,7 +306,7 @@ Lemma range_private_free_left:
   range_private F m1 m' sp base hi.
 Proof.
   intros; red; intros. 
-  destruct (zlt ofs (base + Zmax sz 0)).
+  destruct (zlt ofs (base + Zmax sz 0)) as [z|z].
   red; split. 
   replace ofs with ((ofs - base) + base) by omega.
   eapply Mem.perm_inject; eauto.
@@ -342,7 +342,7 @@ Proof.
   red; intros. exploit RP; eauto. intros [A B].
   destruct UNCH as [U1 U2].
   split. auto. 
-  intros. red in SEP. destruct (F b) as [[sp1 delta1] |]_eqn.
+  intros. red in SEP. destruct (F b) as [[sp1 delta1] |] eqn:?.
   exploit INCR; eauto. intros EQ; rewrite H0 in EQ; inv EQ. 
   red; intros; eelim B; eauto. eapply PERM; eauto. 
   red. destruct (zlt b (Mem.nextblock m1)); auto. 
@@ -710,7 +710,7 @@ Proof.
   induction 1; intros.
   apply match_stacks_nil with bound1; auto. 
     inv MG. constructor; intros; eauto. 
-    destruct (F1 b1) as [[b2' delta']|]_eqn.
+    destruct (F1 b1) as [[b2' delta']|] eqn:?.
     exploit INCR; eauto. intros EQ; rewrite H0 in EQ; inv EQ. eapply IMAGE; eauto. 
     exploit SEP; eauto. intros [A B]. elim B. red. omega. 
   eapply match_stacks_cons; eauto. 
@@ -919,7 +919,7 @@ Proof.
   eapply agree_val_regs; eauto. 
 (* inlined *)
   assert (fd = Internal f0).
-    simpl in H0. destruct (Genv.find_symbol ge id) as [b|]_eqn; try discriminate.
+    simpl in H0. destruct (Genv.find_symbol ge id) as [b|] eqn:?; try discriminate.
     exploit (funenv_program_compat prog); eauto. intros. 
     unfold ge in H0. congruence.
   subst fd.
@@ -973,7 +973,7 @@ Proof.
   eapply Mem.free_left_inject; eauto.
 (* inlined *)
   assert (fd = Internal f0).
-    simpl in H0. destruct (Genv.find_symbol ge id) as [b|]_eqn; try discriminate.
+    simpl in H0. destruct (Genv.find_symbol ge id) as [b|] eqn:?; try discriminate.
     exploit (funenv_program_compat prog); eauto. intros. 
     unfold ge in H0. congruence.
   subst fd.
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v
index 014986d..06826c2 100644
--- a/backend/Inliningspec.v
+++ b/backend/Inliningspec.v
@@ -498,7 +498,7 @@ Proof.
 (* tailcall *)
   destruct (can_inline fe s1) as [|id f P Q].
   (* not inlined *)
-  destruct (retinfo ctx) as [[rpc rreg] | ]_eqn. 
+  destruct (retinfo ctx) as [[rpc rreg] | ] eqn:?. 
   (* turned into a call *)
   eapply tr_tailcall_call; eauto. 
   (* preserved *)
@@ -526,7 +526,7 @@ Proof.
   red; simpl. subst s2; simpl in *; xomega.
   red; auto.
 (* return *)
-  destruct (retinfo ctx) as [[rpc rreg] | ]_eqn. 
+  destruct (retinfo ctx) as [[rpc rreg] | ] eqn:?. 
   (* inlined *)
   eapply tr_return_inlined; eauto. 
   (* unchanged *)
@@ -671,7 +671,7 @@ Lemma transf_function_spec:
   forall f f', transf_function fenv f = OK f' -> tr_function f f'.
 Proof.
   intros. unfold transf_function in H.
-  destruct (expand_function fenv f initstate) as [ctx s i]_eqn. 
+  destruct (expand_function fenv f initstate) as [ctx s i] eqn:?. 
   destruct (zle (st_stksize s) Int.max_unsigned); inv H.
   monadInv Heqr. set (ctx := initcontext x x0 (max_def_function f) (fn_stacksize f)) in *.
 Opaque initstate.
diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index ce7788f..ac47ae8 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -10,7 +10,6 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-open BinPos
 open Coqlib
 open Datatypes
 open LTL
@@ -33,18 +32,6 @@ let enumerate_aux f reach =
 
 (* More clever enumeration that flattens basic blocks *)
 
-let rec int_of_pos = function
-  | Coq_xI p -> (int_of_pos p lsl 1) + 1
-  | Coq_xO p -> int_of_pos p lsl 1
-  | Coq_xH -> 1
-
-let rec pos_of_int n =
-  if n = 0 then assert false else
-  if n = 1 then Coq_xH else
-  if n land 1 = 0
-  then Coq_xO (pos_of_int (n lsr 1))
-  else Coq_xI (pos_of_int (n lsr 1))
-
 module IntSet = Set.Make(struct type t = int let compare = compare end)
 
 (* Determine join points: reachable nodes that have > 1 predecessor *)
@@ -54,7 +41,7 @@ let join_points f =
   let reached = ref IntSet.empty in
   let reached_twice = ref IntSet.empty in
   let rec traverse pc =
-    let npc = int_of_pos pc in
+    let npc = P.to_int pc in
     if IntSet.mem npc !reached then begin
       if not (IntSet.mem npc !reached_twice) then
         reached_twice := IntSet.add npc !reached_twice
@@ -74,14 +61,14 @@ let basic_blocks f joins =
           or a join point
           or the successor of a conditional test *)
   let rec start_block pc =
-    let npc = int_of_pos pc in
+    let npc = P.to_int pc in
     if not (IntSet.mem npc !visited) then begin
       visited := IntSet.add npc !visited;
       in_block [] max_int pc
     end
   (* in_block: add pc to block and check successors *)
   and in_block blk minpc pc =
-    let npc = int_of_pos pc in
+    let npc = P.to_int pc in
     let blk = pc :: blk in
     let minpc = min npc minpc in
     match PTree.get pc f.fn_code with
@@ -103,7 +90,7 @@ let basic_blocks f joins =
   (* next_in_block: check if join point and either extend block
      or start block *)
   and next_in_block blk minpc pc =
-    let npc = int_of_pos pc in
+    let npc = P.to_int pc in
     if IntSet.mem npc joins
     then (end_block blk minpc; start_block pc)
     else in_block blk minpc pc
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index 59178bd..ef6ba1d 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -18,7 +18,6 @@
 open Format
 open Camlcoq
 open Datatypes
-open BinPos
 open Integers
 open AST
 open PrintAST
@@ -212,15 +211,15 @@ let rec print_stmt p s =
       fprintf p "@[<v 3>{{ %a@;<0 -3>}}@]"
               print_stmt s
   | Sexit n ->
-      fprintf p "exit %d;" (camlint_of_nat n)
+      fprintf p "exit %d;" (Nat.to_int n)
   | Sswitch(e, cases, dfl) ->
       fprintf p "@[<v 2>switch (%a) {" print_expr e;
       List.iter
         (fun (n, x) ->
            fprintf p "@ case %ld: exit %d;\n" 
-                     (camlint_of_coqint n) (camlint_of_nat x))
+                     (camlint_of_coqint n) (Nat.to_int x))
         cases;
-      fprintf p "@ default: exit %d;\n" (camlint_of_nat dfl);
+      fprintf p "@ default: exit %d;\n" (Nat.to_int dfl);
       fprintf p "@;<0 -2>}@]"
   | Sreturn None ->
       fprintf p "return;"
@@ -247,7 +246,7 @@ let print_function p id f =
             print_varlist (f.fn_params, true)
             print_sig f.fn_sig;
   fprintf p "@[<v 2>{@ ";
-  let stksz = camlint_of_z f.fn_stackspace in
+  let stksz = Z.to_int32 f.fn_stackspace in
   if stksz <> 0l then
     fprintf p "stack %ld;@ " stksz;
   if f.fn_vars <> [] then
diff --git a/backend/PrintLTLin.ml b/backend/PrintLTLin.ml
index 4dc311c..4e8efd1 100644
--- a/backend/PrintLTLin.ml
+++ b/backend/PrintLTLin.ml
@@ -71,18 +71,18 @@ let print_instruction pp i =
       fprintf pp "%a = builtin %s(%a)@ "
         reg res (name_of_external ef) regs args
   | Llabel lbl ->
-      fprintf pp "%ld:@ " (camlint_of_positive lbl)
+      fprintf pp "%ld:@ " (P.to_int32 lbl)
   | Lgoto lbl ->
-      fprintf pp "goto %ld@ " (camlint_of_positive lbl)
+      fprintf pp "goto %ld@ " (P.to_int32 lbl)
   | Lcond(cond, args, lbl) ->
       fprintf pp "if (%a) goto %ld@ "
         (PrintOp.print_condition reg) (cond, args)
-        (camlint_of_positive lbl)
+        (P.to_int32 lbl)
   | Ljumptable(arg, tbl) ->
       let tbl = Array.of_list tbl in
       fprintf pp "@[<v 2>jumptable (%a)" reg arg;
       for i = 0 to Array.length tbl - 1 do
-        fprintf pp "@ case %d: goto %ld" i (camlint_of_positive tbl.(i))
+        fprintf pp "@ case %d: goto %ld" i (P.to_int32 tbl.(i))
       done;
       fprintf pp "@]@ "
   | Lreturn None ->
diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml
index dfbc66e..7e6c343 100644
--- a/backend/PrintMach.ml
+++ b/backend/PrintMach.ml
@@ -80,18 +80,18 @@ let print_instruction pp i =
   | Mannot(ef, args) ->
       fprintf pp "%s(%a)@ " (name_of_external ef) annot_params args
   | Mlabel lbl ->
-      fprintf pp "%ld:@ " (camlint_of_positive lbl)
+      fprintf pp "%ld:@ " (P.to_int32 lbl)
   | Mgoto lbl ->
-      fprintf pp "goto %ld@ " (camlint_of_positive lbl)
+      fprintf pp "goto %ld@ " (P.to_int32 lbl)
   | Mcond(cond, args, lbl) ->
       fprintf pp "if (%a) goto %ld@ "
         (PrintOp.print_condition reg) (cond, args)
-        (camlint_of_positive lbl)
+        (P.to_int32 lbl)
   | Mjumptable(arg, tbl) ->
       let tbl = Array.of_list tbl in
       fprintf pp "@[<v 2>jumptable (%a)" reg arg;
       for i = 0 to Array.length tbl - 1 do
-        fprintf pp "@ case %d: goto %ld" i (camlint_of_positive tbl.(i))
+        fprintf pp "@ case %d: goto %ld" i (P.to_int32 tbl.(i))
       done;
       fprintf pp "@]@ "
   | Mreturn ->
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
index 4cd3871..0bafcde 100644
--- a/backend/PrintRTL.ml
+++ b/backend/PrintRTL.ml
@@ -25,7 +25,7 @@ open PrintOp
 (* Printing of RTL code *)
 
 let reg pp r =
-  fprintf pp "x%ld" (camlint_of_positive r)
+  fprintf pp "x%ld" (P.to_int32 r)
 
 let rec regs pp = function
   | [] -> ()
@@ -37,14 +37,14 @@ let ros pp = function
   | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
 
 let print_succ pp s dfl =
-  let s = camlint_of_positive s in
+  let s = P.to_int32 s in
   if s <> dfl then fprintf pp "       goto %ld@ " s
 
 let print_instruction pp (pc, i) =
   fprintf pp "%5ld: " pc;
   match i with
   | Inop s ->
-      let s = camlint_of_positive s in
+      let s = P.to_int32 s in
       if s = Int32.pred pc
       then fprintf pp "nop@ "
       else fprintf pp "goto %ld@ " s
@@ -77,12 +77,12 @@ let print_instruction pp (pc, i) =
   | Icond(cond, args, s1, s2) ->
       fprintf pp "if (%a) goto %ld else goto %ld@ "
         (PrintOp.print_condition reg) (cond, args)
-        (camlint_of_positive s1) (camlint_of_positive s2)
+        (P.to_int32 s1) (P.to_int32 s2)
   | Ijumptable(arg, tbl) ->
       let tbl = Array.of_list tbl in
       fprintf pp "@[<v 2>jumptable (%a)" reg arg;
       for i = 0 to Array.length tbl - 1 do
-        fprintf pp "@ case %d: goto %ld" i (camlint_of_positive tbl.(i))
+        fprintf pp "@ case %d: goto %ld" i (P.to_int32 tbl.(i))
       done;
       fprintf pp "@]@ "
   | Ireturn None ->
@@ -96,7 +96,7 @@ let print_function pp id f =
     List.sort
       (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
       (List.map
-        (fun (pc, i) -> (camlint_of_positive pc, i))
+        (fun (pc, i) -> (P.to_int32 pc, i))
         (PTree.elements f.fn_code)) in
   print_succ pp f.fn_entrypoint 
     (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1l);
diff --git a/backend/RREproof.v b/backend/RREproof.v
index 8926fe4..40632f7 100644
--- a/backend/RREproof.v
+++ b/backend/RREproof.v
@@ -248,7 +248,7 @@ Proof.
   induction ll; intros; simpl.
   apply H. simpl. auto.
   apply IHll. intros. unfold Locmap.set. 
-  destruct (Loc.eq a l). auto. destruct (Loc.overlap a l) as []_eqn. auto. 
+  destruct (Loc.eq a l). auto. destruct (Loc.overlap a l) eqn:?. auto. 
   apply H. simpl. split; auto. apply Loc.diff_sym. apply Loc.non_overlap_diff; auto.
 Qed. 
 
@@ -396,7 +396,7 @@ Opaque destroyed_at_move_regs.
   simpl in SAFE. 
   assert (SAFE': sm = false \/ ~In r destroyed_at_move_regs /\ safe_move_insertion b = true).
     destruct (in_dec mreg_eq r destroyed_at_move_regs); simpl in SAFE; intuition congruence. 
-  destruct (is_incoming sl) as []_eqn.
+  destruct (is_incoming sl) eqn:?.
   (* incoming, stays as getstack *)
   assert (UGS: forall rs, undef_getstack sl rs = Locmap.set (R IT1) Vundef rs).
     destruct sl; simpl in Heqb0; discriminate || auto.
@@ -419,11 +419,11 @@ Opaque destroyed_at_move_regs.
   rewrite <- EQ1; rewrite EQ; rewrite EQ2. rewrite locmap_set_reg_same.
   apply match_states_regular with sm; auto; tauto. 
   (* found an equation *)
-  destruct (find_reg_containing sl eqs) as [r'|]_eqn.
+  destruct (find_reg_containing sl eqs) as [r'|] eqn:?.
   exploit EQH. eapply find_reg_containing_sound; eauto. 
   simpl; intro EQ.
   (* turned into a move *)
-  destruct (safe_move_insertion b) as []_eqn. 
+  destruct (safe_move_insertion b) eqn:?. 
   left; econstructor; split. constructor. simpl; eauto. 
   rewrite UGS. rewrite <- EQ.
   apply match_states_regular with true; auto. 
diff --git a/backend/RREtyping.v b/backend/RREtyping.v
index 2501c7f..539fb20 100644
--- a/backend/RREtyping.v
+++ b/backend/RREtyping.v
@@ -91,9 +91,9 @@ Proof.
   assert (WC: wt_code f c) by (red; auto with coqlib).
   clear H.
   inv WI; auto 10 with linearty.
-  destruct (is_incoming s) as []_eqn. auto with linearty.
+  destruct (is_incoming s) eqn:?. auto with linearty.
   destruct (contains_equation s r eqs). auto with linearty.
-  destruct (find_reg_containing s eqs) as [r'|]_eqn; auto with linearty.
+  destruct (find_reg_containing s eqs) as [r'|] eqn:?; auto with linearty.
   assert (mreg_type r' = mreg_type r).
   exploit H0. eapply find_reg_containing_sound; eauto. simpl. congruence.
   destruct (safe_move_insertion c); auto 10 with linearty.
diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v
index 99c89ab..9f5563c 100644
--- a/backend/Reloadtyping.v
+++ b/backend/Reloadtyping.v
@@ -289,7 +289,7 @@ Proof.
   destruct ros. destruct H2 as [A [B C]]. auto 10 with reloadty. 
   auto 10 with reloadty.
 
-  destruct (ef_reloads ef) as [] _eqn.
+  destruct (ef_reloads ef) as [] eqn:?.
   assert (arity_ok (sig_args (ef_sig ef)) = true) by intuition congruence.
   assert (map mreg_type (regs_for args) = map Loc.type args).
     apply wt_regs_for. apply arity_ok_enough. congruence.
diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v
index d086010..4488e49 100644
--- a/backend/Renumberproof.v
+++ b/backend/Renumberproof.v
@@ -91,7 +91,7 @@ Proof.
   (* induction *)
   rewrite PTree.gsspec in H2. unfold renum_node. destruct (peq x k). 
   inv H2. rewrite H3. apply PTree.gss. 
-  destruct f!k as [y'|]_eqn. 
+  destruct f!k as [y'|] eqn:?. 
   rewrite PTree.gso. eauto. red; intros; subst y'. elim n. eapply f_inj; eauto. 
   eauto. 
 Qed.
@@ -111,7 +111,7 @@ Proof.
   intros. 
   destruct (postorder_correct (successors f) f.(fn_entrypoint)) as [A B].
   fold (pnum f) in *. 
-  unfold renum_pc. destruct (pnum f)! pc as [pc'|]_eqn.
+  unfold renum_pc. destruct (pnum f)! pc as [pc'|] eqn:?.
   simpl. eapply renum_cfg_nodes; eauto.
   elim (B pc); auto. unfold successors. rewrite PTree.gmap1. rewrite H. simpl. congruence.
 Qed.
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 09dc0ff..0269438 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -166,10 +166,10 @@ Lemma classify_call_correct:
   end.
 Proof.
   unfold classify_call; intros. 
-  destruct (expr_is_addrof_ident a) as [id|]_eqn. 
+  destruct (expr_is_addrof_ident a) as [id|] eqn:?. 
   exploit expr_is_addrof_ident_correct; eauto. intros EQ; subst a.
   inv H. inv H2. 
-  destruct (Genv.find_symbol ge id) as [b|]_eqn. 
+  destruct (Genv.find_symbol ge id) as [b|] eqn:?. 
   rewrite Genv.find_funct_find_funct_ptr in H0. 
   rewrite H0. 
   destruct fd. exists b; auto. 
@@ -567,7 +567,7 @@ Proof.
     apply call_cont_commut; eauto.
   rewrite H. 
   destruct (find_label lbl (sel_stmt ge (Cminor.fn_body f)) (call_cont k'0))
-  as [[s'' k'']|]_eqn; intros; try contradiction.
+  as [[s'' k'']|] eqn:?; intros; try contradiction.
   destruct H0. 
   left; econstructor; split.
   econstructor; eauto. 
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 6c4e43f..b731487 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -2171,7 +2171,7 @@ Proof.
   exists b; exists tf; split; auto. simpl.
   generalize (AG m0). rewrite EQ. intro INJ. inv INJ.
   inv MG. rewrite DOMAIN in H2. inv H2. simpl. auto. eapply FUNCTIONS; eauto. 
-  destruct (Genv.find_symbol ge i) as [b|]_eqn; try discriminate. 
+  destruct (Genv.find_symbol ge i) as [b|] eqn:?; try discriminate. 
   exploit function_ptr_translated; eauto. intros [tf [A B]].
   exists b; exists tf; split; auto. simpl. 
   rewrite symbols_preserved. auto.
@@ -2398,7 +2398,7 @@ Proof.
   econstructor; split.
   apply plus_one. eapply exec_Mgetparam; eauto. 
   rewrite (unfold_transf_function _ _ TRANSL). unfold fn_link_ofs. 
-  eapply index_contains_load_stack with (idx := FI_link). eauto. eapply agree_link; eauto. 
+  eapply index_contains_load_stack with (idx := FI_link). eapply TRANSL. eapply agree_link; eauto.
   simpl parent_sp.
   change (offset_of_index (make_env (function_bounds f)) (FI_arg z t))
     with (offset_of_index (make_env (function_bounds f0)) (FI_arg z t)).