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

5 files changed, 66 insertions, 66 deletions

diff --git a/common/AST.v b/common/AST.v
index 40da732..d2065d6 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -225,10 +225,10 @@ Proof.
   revert x EQ H0. induction (prog_defs p); simpl; intros.
   inv EQ. contradiction.
   destruct a as [id [f|v]].
-  destruct (transf_fun f) as [tf1|msg]_eqn; monadInv EQ.
+  destruct (transf_fun f) as [tf1|msg] eqn:?; monadInv EQ.
   simpl in H0; destruct H0. inv H. exists f; auto. 
   exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto.
-  destruct (transf_globvar v) as [tv1|msg]_eqn; monadInv EQ.
+  destruct (transf_globvar v) as [tv1|msg] eqn:?; monadInv EQ.
   simpl in H0; destruct H0. inv H.
   exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto.
 Qed.
@@ -245,10 +245,10 @@ Proof.
   revert x EQ H0. induction (prog_defs p); simpl; intros.
   inv EQ. contradiction.
   destruct a as [id [f|v]].
-  destruct (transf_fun f) as [tf1|msg]_eqn; monadInv EQ.
+  destruct (transf_fun f) as [tf1|msg] eqn:?; monadInv EQ.
   simpl in H0; destruct H0. inv H.
   exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto.
-  destruct (transf_globvar v) as [tv1|msg]_eqn; monadInv EQ.
+  destruct (transf_globvar v) as [tv1|msg] eqn:?; monadInv EQ.
   simpl in H0; destruct H0. inv H.
   monadInv Heqr. simpl. exists (gvar_info v). split. left. destruct v; auto. auto.
   exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto.
@@ -394,11 +394,11 @@ Proof.
   monadInv EQ. constructor.
   destruct a as [id [f|v]]. 
   (* function *)
-  destruct (transf_fun f) as [tf|?]_eqn; monadInv EQ. 
+  destruct (transf_fun f) as [tf|?] eqn:?; monadInv EQ. 
   constructor; auto. constructor; auto.
   (* variable *)
   unfold transf_globvar in EQ.
-  destruct (transf_var (gvar_info v)) as [tinfo|?]_eqn; simpl in EQ; monadInv EQ.
+  destruct (transf_var (gvar_info v)) as [tinfo|?] eqn:?; simpl in EQ; monadInv EQ.
   constructor; auto. destruct v; simpl in *. constructor; auto.
 Qed.
 
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index 100cab8..d426440 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -607,14 +607,14 @@ Proof.
   unfold alloc_global. intros.
   destruct g as [id [f|v]]. 
   (* function *)
-  destruct (Mem.alloc m 0 1) as [m1 b]_eqn.
+  destruct (Mem.alloc m 0 1) as [m1 b] eqn:?.
   erewrite Mem.nextblock_drop; eauto. erewrite Mem.nextblock_alloc; eauto. 
   (* variable *)
   set (init := gvar_init v) in *.
   set (sz := init_data_list_size init) in *.
-  destruct (Mem.alloc m 0 sz) as [m1 b]_eqn.
-  destruct (store_zeros m1 b 0 sz) as [m2|]_eqn; try discriminate.
-  destruct (store_init_data_list m2 b 0 init) as [m3|]_eqn; try discriminate.
+  destruct (Mem.alloc m 0 sz) as [m1 b] eqn:?.
+  destruct (store_zeros m1 b 0 sz) as [m2|] eqn:?; try discriminate.
+  destruct (store_init_data_list m2 b 0 init) as [m3|] eqn:?; try discriminate.
   erewrite Mem.nextblock_drop; eauto.
   erewrite store_init_data_list_nextblock; eauto.
   erewrite store_zeros_nextblock; eauto.
@@ -629,7 +629,7 @@ Proof.
   induction gl.
   simpl; intros. inv H; unfold block; omega.
   simpl length; rewrite inj_S; simpl; intros.
-  destruct (alloc_global m a) as [m1|]_eqn; try discriminate.
+  destruct (alloc_global m a) as [m1|] eqn:?; try discriminate.
   erewrite IHgl; eauto. erewrite alloc_global_nextblock; eauto. unfold block; omega.
 Qed.
 
@@ -672,7 +672,7 @@ Remark alloc_global_perm:
 Proof.
   intros. destruct idg as [id [f|v]]; simpl in H. 
   (* function *)
-  destruct (Mem.alloc m 0 1) as [m1 b]_eqn. 
+  destruct (Mem.alloc m 0 1) as [m1 b] eqn:?. 
   assert (b' <> b). apply Mem.valid_not_valid_diff with m; eauto with mem.
   split; intros.
   eapply Mem.perm_drop_3; eauto. eapply Mem.perm_alloc_1; eauto. 
@@ -680,9 +680,9 @@ Proof.
   (* variable *)
   set (init := gvar_init v) in *.
   set (sz := init_data_list_size init) in *.
-  destruct (Mem.alloc m 0 sz) as [m1 b]_eqn.
-  destruct (store_zeros m1 b 0 sz) as [m2|]_eqn; try discriminate.
-  destruct (store_init_data_list m2 b 0 init) as [m3|]_eqn; try discriminate.
+  destruct (Mem.alloc m 0 sz) as [m1 b] eqn:?.
+  destruct (store_zeros m1 b 0 sz) as [m2|] eqn:?; try discriminate.
+  destruct (store_init_data_list m2 b 0 init) as [m3|] eqn:?; try discriminate.
   assert (b' <> b). apply Mem.valid_not_valid_diff with m; eauto with mem.
   split; intros.
   eapply Mem.perm_drop_3; eauto.
@@ -703,7 +703,7 @@ Remark alloc_globals_perm:
 Proof.
   induction gl.
   simpl; intros. inv H. tauto.
-  simpl; intros. destruct (alloc_global m a) as [m1|]_eqn; try discriminate.
+  simpl; intros. destruct (alloc_global m a) as [m1|] eqn:?; try discriminate.
   erewrite alloc_global_perm; eauto. eapply IHgl; eauto. 
   unfold Mem.valid_block in *. erewrite alloc_global_nextblock; eauto. omega. 
 Qed.
@@ -734,7 +734,7 @@ Remark store_init_data_list_outside:
 Proof.
   induction il; simpl.
   intros; congruence.
-  intros. destruct (store_init_data m b p a) as [m1|]_eqn; try congruence.
+  intros. destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence.
   transitivity (Mem.load chunk m1 b' q).
   eapply IHil; eauto. generalize (init_data_size_pos a). intuition omega.
   destruct a; simpl in Heqo;
@@ -784,7 +784,7 @@ Proof.
 
   induction il; simpl.
   auto.
-  intros. destruct (store_init_data m b p a) as [m1|]_eqn; try congruence.
+  intros. destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence.
   exploit IHil; eauto. intro D. 
   destruct a; simpl in Heqo; intuition.
   eapply (A Mint8unsigned (Vint i)); eauto.
@@ -804,7 +804,7 @@ Remark load_alloc_global:
 Proof.
   intros. destruct g as [f|v]; simpl in H.
   (* function *)
-  destruct (Mem.alloc m 0 1) as [m1 b']_eqn. 
+  destruct (Mem.alloc m 0 1) as [m1 b'] eqn:?. 
   assert (b <> b'). apply Mem.valid_not_valid_diff with m; eauto with mem.
   transitivity (Mem.load chunk m1 b p). 
   eapply Mem.load_drop; eauto. 
@@ -812,9 +812,9 @@ Proof.
   (* variable *)
   set (init := gvar_init v) in *.
   set (sz := init_data_list_size init) in *.
-  destruct (Mem.alloc m 0 sz) as [m1 b']_eqn.
-  destruct (store_zeros m1 b' 0 sz) as [m2|]_eqn; try discriminate.
-  destruct (store_init_data_list m2 b' 0 init) as [m3|]_eqn; try discriminate.
+  destruct (Mem.alloc m 0 sz) as [m1 b'] eqn:?.
+  destruct (store_zeros m1 b' 0 sz) as [m2|] eqn:?; try discriminate.
+  destruct (store_init_data_list m2 b' 0 init) as [m3|] eqn:?; try discriminate.
   assert (b <> b'). apply Mem.valid_not_valid_diff with m; eauto with mem.
   transitivity (Mem.load chunk m3 b p). 
   eapply Mem.load_drop; eauto.
@@ -833,7 +833,7 @@ Remark load_alloc_globals:
 Proof.
   induction gl; simpl; intros.
   congruence.
-  destruct (alloc_global m a) as [m''|]_eqn; try discriminate.
+  destruct (alloc_global m a) as [m''|] eqn:?; try discriminate.
   transitivity (Mem.load chunk m'' b p). 
   apply IHgl; auto. unfold Mem.valid_block in *. 
   erewrite alloc_global_nextblock; eauto. omega.
@@ -895,9 +895,9 @@ Proof.
   inv H3. simpl in H0.
   set (init := gvar_init gv) in *.
   set (sz := init_data_list_size init) in *.
-  destruct (Mem.alloc m 0 sz) as [m1 b']_eqn.
-  destruct (store_zeros m1 b' 0 sz) as [m2|]_eqn; try discriminate.
-  destruct (store_init_data_list m2 b' 0 init) as [m3|]_eqn; try discriminate.
+  destruct (Mem.alloc m 0 sz) as [m1 b'] eqn:?.
+  destruct (store_zeros m1 b' 0 sz) as [m2|] eqn:?; try discriminate.
+  destruct (store_init_data_list m2 b' 0 init) as [m3|] eqn:?; try discriminate.
   exploit Mem.alloc_result; eauto. intro RES. 
   replace (genv_next ge0) with b' by congruence.
   split. red; intros. eapply Mem.perm_drop_1; eauto.
@@ -928,7 +928,7 @@ Proof.
   destruct (ZIndexed.eq b (genv_next ge0)).
   (* same *)
   inv H3. simpl in H0. 
-  destruct (Mem.alloc m 0 1) as [m1 b']_eqn. 
+  destruct (Mem.alloc m 0 1) as [m1 b'] eqn:?. 
   exploit Mem.alloc_result; eauto. intro RES. 
   replace (genv_next ge0) with b' by congruence.
   split. eapply Mem.perm_drop_1; eauto. omega. 
@@ -964,7 +964,7 @@ Lemma alloc_globals_initialized:
 Proof.
   induction gl; simpl; intros.
   inv H0; auto.
-  destruct a as [id g]. destruct (alloc_global m (id, g)) as [m1|]_eqn; try discriminate.
+  destruct a as [id g]. destruct (alloc_global m (id, g)) as [m1|] eqn:?; try discriminate.
   exploit alloc_global_initialized; eauto. intros [P [Q R]].
   eapply IHgl; eauto. 
 Qed.
@@ -1099,16 +1099,16 @@ Lemma alloc_global_neutral:
 Proof.
   intros. destruct idg as [id [f|v]]; simpl in H.
   (* function *)
-  destruct (Mem.alloc m 0 1) as [m1 b]_eqn.
+  destruct (Mem.alloc m 0 1) as [m1 b] eqn:?.
   assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
   eapply Mem.drop_inject_neutral; eauto. 
   eapply Mem.alloc_inject_neutral; eauto.
   (* variable *)
   set (init := gvar_init v) in *.
   set (sz := init_data_list_size init) in *.
-  destruct (Mem.alloc m 0 sz) as [m1 b]_eqn.
-  destruct (store_zeros m1 b 0 sz) as [m2|]_eqn; try discriminate.
-  destruct (store_init_data_list ge m2 b 0 init) as [m3|]_eqn; try discriminate.
+  destruct (Mem.alloc m 0 sz) as [m1 b] eqn:?.
+  destruct (store_zeros m1 b 0 sz) as [m2|] eqn:?; try discriminate.
+  destruct (store_init_data_list ge m2 b 0 init) as [m3|] eqn:?; try discriminate.
   assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
   eapply Mem.drop_inject_neutral; eauto. 
   eapply store_init_data_list_neutral with (m := m2) (b := b); eauto.
@@ -1210,7 +1210,7 @@ Lemma alloc_global_augment:
 Proof.
   intros. destruct idg as [id [f|v]]; simpl in H.
   (* function *)
-  destruct (Mem.alloc m2 0 1) as [m3 b]_eqn.
+  destruct (Mem.alloc m2 0 1) as [m3 b] eqn:?.
   assert (b >= thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
   eapply Mem.drop_outside_inject. 2: eauto. 
   eapply Mem.alloc_right_inject; eauto.
@@ -1219,9 +1219,9 @@ Proof.
   (* variable *)
   set (init := gvar_init v) in *.
   set (sz := init_data_list_size init) in *.
-  destruct (Mem.alloc m2 0 sz) as [m3 b]_eqn.
-  destruct (store_zeros m3 b 0 sz) as [m4|]_eqn; try discriminate.
-  destruct (store_init_data_list ge m4 b 0 init) as [m5|]_eqn; try discriminate.
+  destruct (Mem.alloc m2 0 sz) as [m3 b] eqn:?.
+  destruct (store_zeros m3 b 0 sz) as [m4|] eqn:?; try discriminate.
+  destruct (store_init_data_list ge m4 b 0 init) as [m5|] eqn:?; try discriminate.
   assert (b >= thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
   eapply Mem.drop_outside_inject. 2: eauto. 
   eapply store_init_data_list_augment. 3: eauto. 2: eauto.
@@ -1497,7 +1497,7 @@ Proof.
   assert (forall m', store_init_data (globalenv p) m b ofs a = Some m' ->
           store_init_data (globalenv p') m b ofs a = Some m').
    destruct a; simpl; auto. rewrite find_symbol_match. auto.
-   simpl in H. destruct (find_symbol (globalenv p) i) as [b'|]_eqn; try discriminate.
+   simpl in H. destruct (find_symbol (globalenv p) i) as [b'|] eqn:?; try discriminate.
    apply new_ids_fresh. congruence.
   case_eq (store_init_data (globalenv p) m b ofs a); intros. 
     rewrite H1 in H. 
@@ -1513,14 +1513,14 @@ Lemma alloc_globals_match:
 Proof.
   induction 1; simpl; intros.
   auto.
-  destruct (alloc_global (globalenv p) m a1) as [m1|]_eqn; try discriminate.
+  destruct (alloc_global (globalenv p) m a1) as [m1|] eqn:?; try discriminate.
   assert (alloc_global (globalenv p') m b1 = Some m1).
     inv H; simpl in *. 
     auto.
     set (sz := init_data_list_size init) in *.
-    destruct (Mem.alloc m 0 sz) as [m2 b]_eqn.
-    destruct (store_zeros m2 b 0 sz) as [m3|]_eqn; try discriminate.
-    destruct (store_init_data_list (globalenv p) m3 b 0 init) as [m4|]_eqn; try discriminate.
+    destruct (Mem.alloc m 0 sz) as [m2 b] eqn:?.
+    destruct (store_zeros m2 b 0 sz) as [m3|] eqn:?; try discriminate.
+    destruct (store_init_data_list (globalenv p) m3 b 0 init) as [m4|] eqn:?; try discriminate.
     erewrite store_init_data_list_match; eauto. 
   rewrite H2. eauto.
 Qed.
@@ -1718,7 +1718,7 @@ Hypothesis transf_OK:
 Remark transf_augment_OK:
   transform_partial_augment_program transf_fun transf_var nil p.(prog_main) p = OK p'.
 Proof.
-  rewrite <- transf_OK. apply symmetry. apply transform_partial_program2_augment.
+  rewrite <- transf_OK. symmetry. apply transform_partial_program2_augment.
 Qed.
 
 Theorem find_funct_ptr_transf_partial2:
diff --git a/common/Memory.v b/common/Memory.v
index 37f21d7..514e1e0 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -1023,7 +1023,7 @@ Proof.
   decEq. rewrite store_mem_contents; simpl.
   rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'.
   destruct H. congruence.
-  destruct (zle n 0). 
+  destruct (zle n 0) as [z | n0].
   rewrite (nat_of_Z_neg _ z). auto.
   destruct H. omegaContradiction.
   apply getN_setN_outside. rewrite encode_val_length. rewrite <- size_chunk_conv.
@@ -1108,7 +1108,7 @@ Proof.
     assert (length mvl = sz). 
       generalize (encode_val_length chunk v). rewrite <- H1. rewrite SZ. 
       simpl; congruence.
-    rewrite H4. rewrite size_chunk_conv in z0. omega. 
+    rewrite H4. rewrite size_chunk_conv in *. omega.
   contradiction.
 
 (* 3. ofs > ofs':
@@ -1126,8 +1126,8 @@ Proof.
     rewrite setN_outside. rewrite ZMap.gss. auto. omega.
   assert (~memval_valid_first (c'#ofs)).
     rewrite SZ' in PSHAPE. simpl in PSHAPE. inv PSHAPE. 
-    apply H4. apply getN_in. rewrite size_chunk_conv in z. 
-    rewrite SZ' in z. rewrite inj_S in z. omega. 
+    apply H4. apply getN_in. rewrite size_chunk_conv in *.
+    rewrite SZ' in *. rewrite inj_S in *. omega.
   contradiction.
 Qed.
 
@@ -3632,18 +3632,18 @@ Lemma mem_inj_compose:
 Proof.
   intros. unfold compose_meminj. inv H; inv H0; constructor; intros.
   (* perm *)
-  destruct (f b1) as [[b' delta'] |]_eqn; try discriminate.
-  destruct (f' b') as [[b'' delta''] |]_eqn; inv H. 
+  destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate.
+  destruct (f' b') as [[b'' delta''] |] eqn:?; inv H. 
   replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') by omega.
   eauto.
   (* valid access *)
-  destruct (f b1) as [[b' delta'] |]_eqn; try discriminate.
-  destruct (f' b') as [[b'' delta''] |]_eqn; inv H. 
+  destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate.
+  destruct (f' b') as [[b'' delta''] |] eqn:?; inv H. 
   replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') by omega.
   eauto.
   (* memval *)
-  destruct (f b1) as [[b' delta'] |]_eqn; try discriminate.
-  destruct (f' b') as [[b'' delta''] |]_eqn; inv H. 
+  destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate.
+  destruct (f' b') as [[b'' delta''] |] eqn:?; inv H. 
   replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') by omega.
   eapply memval_inject_compose; eauto.
 Qed. 
@@ -3661,15 +3661,15 @@ Proof.
   intros. erewrite mi_freeblocks0; eauto. 
 (* mapped *)
   intros. 
-  destruct (f b) as [[b1 delta1] |]_eqn; try discriminate.
-  destruct (f' b1) as [[b2 delta2] |]_eqn; inv H. 
+  destruct (f b) as [[b1 delta1] |] eqn:?; try discriminate.
+  destruct (f' b1) as [[b2 delta2] |] eqn:?; inv H. 
   eauto.
 (* no overlap *)
   red; intros. 
-  destruct (f b1) as [[b1x delta1x] |]_eqn; try discriminate.
-  destruct (f' b1x) as [[b1y delta1y] |]_eqn; inv H0. 
-  destruct (f b2) as [[b2x delta2x] |]_eqn; try discriminate.
-  destruct (f' b2x) as [[b2y delta2y] |]_eqn; inv H1.
+  destruct (f b1) as [[b1x delta1x] |] eqn:?; try discriminate.
+  destruct (f' b1x) as [[b1y delta1y] |] eqn:?; inv H0. 
+  destruct (f b2) as [[b2x delta2x] |] eqn:?; try discriminate.
+  destruct (f' b2x) as [[b2y delta2y] |] eqn:?; inv H1.
   exploit mi_no_overlap0; eauto. intros A.
   destruct (eq_block b1x b2x). 
   subst b1x. destruct A. congruence. 
@@ -3680,8 +3680,8 @@ Proof.
   unfold block; omega.
 (* representable *)
   intros. 
-  destruct (f b) as [[b1 delta1] |]_eqn; try discriminate.
-  destruct (f' b1) as [[b2 delta2] |]_eqn; inv H. 
+  destruct (f b) as [[b1 delta1] |] eqn:?; try discriminate.
+  destruct (f' b1) as [[b2 delta2] |] eqn:?; inv H. 
   exploit mi_representable0; eauto. intros [A B].
   set (ofs' := Int.repr (Int.unsigned ofs + delta1)).
   assert (Int.unsigned ofs' = Int.unsigned ofs + delta1). 
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index 53741d5..7f2ed3f 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -42,7 +42,7 @@ let name_of_external = function
   | EF_malloc -> "malloc"
   | EF_free -> "free"
   | EF_memcpy(sz, al) ->
-      sprintf "memcpy size %ld align %ld " (camlint_of_z sz) (camlint_of_z al)
+      sprintf "memcpy size %s align %s " (Z.to_string sz) (Z.to_string al)
   | EF_annot(text, targs) -> sprintf "annot %S" (extern_atom text)
   | EF_annot_val(text, targ) ->  sprintf "annot_val %S" (extern_atom text)
   | EF_inline_asm text -> sprintf "inline_asm %S" (extern_atom text)
diff --git a/common/Values.v b/common/Values.v
index 1c03789..177cd93 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -620,7 +620,7 @@ Theorem modu_divu:
   modu x y = Some z -> exists v, divu x y = Some v /\ z = sub x (mul v y).
 Proof.
   intros. destruct x; destruct y; simpl in *; try discriminate.
-  destruct (Int.eq i0 Int.zero) as []_eqn; inv H. 
+  destruct (Int.eq i0 Int.zero) eqn:?; inv H. 
   exists (Vint (Int.divu i i0)); split; auto. 
   simpl. rewrite Int.modu_divu. auto.
   generalize (Int.eq_spec i0 Int.zero). rewrite Heqb; auto. 
@@ -731,7 +731,7 @@ Theorem shrx_carry:
   add (shr x y) (shr_carry x y) = z.
 Proof.
   intros. destruct x; destruct y; simpl in H; inv H. 
-  destruct (Int.ltu i0 (Int.repr 31)) as []_eqn; inv H1.
+  destruct (Int.ltu i0 (Int.repr 31)) eqn:?; inv H1.
   exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31. intros.
   assert (Int.ltu i0 Int.iwordsize = true). 
     unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. omega. 
@@ -746,7 +746,7 @@ Theorem shrx_shr:
     z = shr (if Int.lt p Int.zero then add x (Vint (Int.sub (Int.shl Int.one q) Int.one)) else x) (Vint q).
 Proof.
   intros. destruct x; destruct y; simpl in H; inv H. 
-  destruct (Int.ltu i0 (Int.repr 31)) as []_eqn; inv H1.
+  destruct (Int.ltu i0 (Int.repr 31)) eqn:?; inv H1.
   exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31. intros.
   assert (Int.ltu i0 Int.iwordsize = true). 
     unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. omega. 
@@ -1030,8 +1030,8 @@ Proof.
   destruct v1; simpl in H2; try discriminate;
   destruct v2; simpl in H2; try discriminate;
   inv H0; inv H1; simpl; auto.
-  destruct (valid_ptr b0 (Int.unsigned i)) as []_eqn; try discriminate.
-  destruct (valid_ptr b1 (Int.unsigned i0)) as []_eqn; try discriminate.
+  destruct (valid_ptr b0 (Int.unsigned i)) eqn:?; try discriminate.
+  destruct (valid_ptr b1 (Int.unsigned i0)) eqn:?; try discriminate.
   rewrite (H _ _ Heqb2). rewrite (H _ _ Heqb0). auto.
 Qed.