Glasnost: making transparent a number of definitions that were opaque

for no good reason.



git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2140 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

29 files changed, 133 insertions, 120 deletions

diff --git a/Changelog b/Changelog
index 670a6d0..5bf7335 100644
--- a/Changelog
+++ b/Changelog
@@ -17,6 +17,9 @@ Development version
   that are passed on the call stack.
 - ARM port; slightly better code generated for some indirect memory
   accesses.
+- Coq cleanups: a number of definitions that were opaque for no good reason
+  are now properly transparent.
+
 
 Release 1.12.1, 2013-01-29
 ==========================
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index dcae740..0760eb0 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -261,7 +261,7 @@ Qed.
 Remark transl_op_label:
   forall op args r k c, transl_op op args r k = OK c -> tail_nolabel k c.
 Proof.
-Opaque Int.repr Int.eq.
+Opaque Int.eq.
   unfold transl_op; intros; destruct op; TailNoLabel.
   destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
   destruct (ireg_eq x x0 || ireg_eq x x1); TailNoLabel.
@@ -671,7 +671,6 @@ Opaque loadind.
   Simpl. rewrite <- H2. auto.
 
 - (* Mtailcall *)
-Opaque Int.repr.
   assert (f0 = f) by congruence.  subst f0.
   inversion AT; subst.
   assert (NOOV: list_length_z (fn_code tf) <= Int.max_unsigned).
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 9d90d1f..06d6d17 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -813,8 +813,8 @@ Proof.
   split. unfold rs3. Simpl. 
   replace (rs2 (crbit_for_cond cmp)) with (rs1 (crbit_for_cond cmp)).
   destruct (eval_condition cmp rs##(preg_of##args) m) as [[]|]; simpl in *.
-  rewrite B. simpl. Simpl. 
-  rewrite B. simpl. unfold rs2. Simpl.
+  rewrite B. simpl. rewrite Int.eq_false. Simpl. apply Int.one_not_zero.  
+  rewrite B. simpl. rewrite Int.eq_true. unfold rs2. Simpl.
   auto.
   destruct cmp; reflexivity. 
   intros. transitivity (rs2 r). 
diff --git a/arm/Machregs.v b/arm/Machregs.v
index f5b5329..317515c 100644
--- a/arm/Machregs.v
+++ b/arm/Machregs.v
@@ -45,7 +45,7 @@ Inductive mreg: Type :=
   | FT1: mreg (* F6 *) | FT2: mreg (* F7 *).
 
 Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}.
-Proof. decide equality. Qed.
+Proof. decide equality. Defined.
 
 Definition mreg_type (r: mreg): typ :=
   match r with
diff --git a/arm/Op.v b/arm/Op.v
index 291d64f..06d0705 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -137,7 +137,7 @@ Proof.
   subst x. rewrite (proof_irr Px Py). left; auto.
   right. red; intro. elim n. inversion H0. auto.
   decide equality.
-Qed.
+Defined.
 
 Definition eq_operation (x y: operation): {x=y} + {x<>y}.
 Proof.
@@ -148,14 +148,16 @@ Proof.
   assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality.
   assert (forall (x y: condition), {x=y}+{x<>y}). decide equality.
   decide equality.
-Qed.
+Defined.
 
 Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}.
 Proof.
   generalize Int.eq_dec; intro.
   generalize eq_shift; intro.
   decide equality.
-Qed.
+Defined.
+
+Global Opaque eq_shift eq_operation eq_addressing.
 
 (** * Evaluation functions *)
 
diff --git a/backend/CSE.v b/backend/CSE.v
index 1888fb8..45a804e 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -60,9 +60,7 @@ Inductive rhs : Type :=
 Definition eq_valnum: forall (x y: valnum), {x=y}+{x<>y} := peq.
 
 Definition eq_list_valnum (x y: list valnum) : {x=y}+{x<>y}.
-Proof.
-  decide equality. apply eq_valnum.
-Qed.
+Proof. decide equality. apply eq_valnum. Defined.
 
 Definition eq_rhs (x y: rhs) : {x=y}+{x<>y}.
 Proof.
@@ -74,7 +72,7 @@ Proof.
   generalize eq_valnum; intro.
   generalize eq_list_valnum; intro.
   decide equality.
-Qed.
+Defined.
 
 (** A value numbering is a collection of equations between value numbers
   plus a partial map from registers to value numbers.  Additionally,
diff --git a/backend/Constprop.v b/backend/Constprop.v
index 8fa0691..2f3123f 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -49,7 +49,7 @@ Module Approx <: SEMILATTICE_WITH_TOP.
     apply Int.eq_dec.
     apply ident_eq.
     apply Int.eq_dec.
-  Qed.
+  Defined.
   Definition beq (x y: t) := if eq_dec x y then true else false.
   Lemma beq_correct: forall x y, beq x y = true -> x = y.
   Proof.
diff --git a/backend/Locations.v b/backend/Locations.v
index ba2fb06..2381fea 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -89,7 +89,8 @@ Proof.
   decide equality.
   generalize zeq; intro.
   decide equality.
-Qed.
+Defined.
+Global Opaque slot_eq.
 
 Open Scope Z_scope.
 
@@ -122,7 +123,7 @@ Module Loc.
   Lemma eq: forall (p q: loc), {p = q} + {p <> q}.
   Proof.
     decide equality. apply mreg_eq. apply slot_eq.
-  Qed.
+  Defined.
 
 (** As mentioned previously, two locations can be different (in the sense
   of the [<>] mathematical disequality), yet denote 
@@ -286,7 +287,7 @@ Module Loc.
     case_eq (overlap l1 l2); intros.
     right. apply overlap_not_diff; auto.
     left. apply non_overlap_diff; auto.
-  Qed.
+  Defined.
 
 (** We now redefine some standard notions over lists, using the [Loc.diff]
   predicate instead of standard disequality [<>].
@@ -383,6 +384,8 @@ Module Loc.
 
 End Loc.
 
+Global Opaque Loc.eq Loc.diff_dec.
+
 (** * Mappings from locations to values *)
 
 (** The [Locmap] module defines mappings from locations to values,
diff --git a/backend/RRE.v b/backend/RRE.v
index ece6051..b8409e3 100644
--- a/backend/RRE.v
+++ b/backend/RRE.v
@@ -37,7 +37,7 @@ Fixpoint find_reg_containing (s: slot) (eqs: equations) : option mreg :=
 Definition eq_equation (eq1 eq2: equation) : {eq1=eq2} + {eq1<>eq2}.
 Proof.
   generalize slot_eq mreg_eq. decide equality.
-Qed.
+Defined.
 
 Definition contains_equation (s: slot) (r: mreg) (eqs: equations) : bool :=
   In_dec eq_equation (mkeq r s) eqs.
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index 1d49909..6402237 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -267,8 +267,8 @@ Proof.
   destruct s; unfold undef_getstack; unfold loc_acceptable in H; auto.
   apply Locmap.gso. tauto.
   apply Loc.diff_sym. simpl in H0; unfold t; destruct (slot_type s); tauto.
-  rewrite Locmap.gso. unfold undef_getstack. destruct s; auto. 
-  apply Locmap.gso. red; congruence.
+  rewrite Locmap.gso. unfold undef_getstack. 
+  destruct s; simpl in H; reflexivity || contradiction. 
   unfold t; destruct (slot_type s); red; congruence.
 Qed.
 
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 4ce8c25..d97ec93 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -779,9 +779,6 @@ Lemma agree_frame_set_reg:
 Proof.
   intros. inv H; constructor; auto; intros.
   rewrite Locmap.gso. auto. red. intuition congruence.
-  rewrite Locmap.gso; auto. red; auto.
-  rewrite Locmap.gso; auto. red; auto.
-  rewrite Locmap.gso; auto. red; auto.
   apply wt_setloc; auto.
 Qed.
 
@@ -857,8 +854,6 @@ Proof.
   intros. inv H. 
   change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_local ofs ty))) in H3.
   constructor; auto; intros.
-(* unused *)
-  rewrite Locmap.gso; auto. red; auto.
 (* local *)
   unfold Locmap.set. simpl. destruct (Loc.eq (S (Local ofs ty)) (S (Local ofs0 ty0))).
   inv e. eapply gss_index_contains_inj; eauto. 
@@ -867,8 +862,6 @@ Proof.
 (* outgoing *)
   rewrite Locmap.gso. eapply gso_index_contains_inj; eauto with stacking.
   simpl; auto. red; auto.
-(* incoming *)
-  rewrite Locmap.gso; auto. red; auto.
 (* parent *)
   eapply gso_index_contains; eauto. red; auto.
 (* retaddr *)
@@ -899,8 +892,6 @@ Proof.
   intros. inv H. 
   change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_arg ofs ty))) in H3.
   constructor; auto; intros.
-(* unused *)
-  rewrite Locmap.gso; auto. red; auto.
 (* local *)
   rewrite Locmap.gso. eapply gso_index_contains_inj; eauto. simpl; auto. red; auto.
 (* outgoing *)
@@ -911,8 +902,6 @@ Proof.
   red; intros. eapply Mem.perm_store_1; eauto.
   eapply gso_index_contains_inj; eauto.
   red. eapply Loc.overlap_aux_false_1; eauto.
-(* incoming *)
-  rewrite Locmap.gso; auto. red; auto.
 (* parent *)
   eapply gso_index_contains; eauto with stacking. red; auto.
 (* retaddr *)
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index c638259..ebc27ad 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -92,7 +92,7 @@ Fixpoint is_val_list (al: exprlist) : option (list (val * type)) :=
 Definition is_skip (s: statement) : {s = Sskip} + {s <> Sskip}.
 Proof.
   destruct s; (left; congruence) || (right; congruence).
-Qed.
+Defined.
 
 (** * Events, volatile memory accesses, and external functions. *)
 
@@ -303,7 +303,7 @@ Proof with try (right; intuition omega).
   destruct (zle (Int.unsigned ofs + sizeof ty) (Int.unsigned ofs')); auto.
   right; intuition omega.
   destruct Y... left; intuition omega. 
-Qed.
+Defined.
 
 Definition do_assign_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) (v: val): option (world * trace * mem) :=
   match access_mode ty with
@@ -464,7 +464,7 @@ Proof with try (right; intuition omega).
     destruct (zle (odst + sz) osrc); auto.
     right; intuition omega.
   destruct Y... left; intuition omega.
-Qed.
+Defined.
 
 Definition do_ef_memcpy (sz al: Z)
        (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
@@ -2180,7 +2180,6 @@ Proof with (unfold ret; auto with coqlib).
   rewrite H0...
   rewrite H0...
   rewrite pred_dec_false...
-  rewrite pred_dec_true...
   rewrite H0...
   rewrite H0...
   destruct H0; subst x...
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 9d518cb..51f89da 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -486,11 +486,8 @@ Definition transl_function (f: Clight.function) : res function :=
        (map fst (Clight.fn_temps f))
        tbody).
 
-Definition list_typ_eq:
-  forall (l1 l2: list typ), {l1=l2} + {l1<>l2}.
-Proof.
-  generalize typ_eq; intro. decide equality. 
-Qed.
+Definition list_typ_eq: forall (l1 l2: list typ), {l1=l2} + {l1<>l2}
+                     := list_eq_dec typ_eq.
 
 Definition transl_fundef (f: Clight.fundef) : res fundef :=
   match f with
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index b64c309..b0884ac 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -397,13 +397,11 @@ Proof.
 Opaque zeq.
   intros. unfold sem_cmp in *.
   destruct (classify_cmp ty1 ty2); try (destruct s); inv H1; inv H2; inv H; inv H0; auto with mval.
-  destruct (Int.eq n Int.zero); try discriminate. 
+- destruct (Int.eq n Int.zero); try discriminate. 
   unfold Val.cmp_different_blocks in *. destruct c; inv H3; inv H2; constructor.
-  destruct (Int.eq n Int.zero); try discriminate. 
+- destruct (Int.eq n Int.zero); try discriminate. 
   unfold Val.cmp_different_blocks in *. destruct c; inv H2; inv H1; constructor.
-  rewrite (mem_empty_not_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4.
-  rewrite (mem_empty_not_weak_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4. simpl in H4.
-  destruct (zeq (Z.pos id) (Z.pos id0)); discriminate.
+- destruct (zeq (Z.pos id) (Z.pos id0)); discriminate.
 Qed.
 
 Lemma sem_binary_match:
diff --git a/common/AST.v b/common/AST.v
index 44811b2..8595b95 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -47,10 +47,12 @@ Lemma typesize_pos: forall ty, typesize ty > 0.
 Proof. destruct ty; simpl; omega. Qed.
 
 Lemma typ_eq: forall (t1 t2: typ), {t1=t2} + {t1<>t2}.
-Proof. decide equality. Qed.
+Proof. decide equality. Defined.
+Global Opaque typ_eq.
 
 Lemma opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2}.
-Proof. decide equality. apply typ_eq. Qed.
+Proof. decide equality. apply typ_eq. Defined.
+Global Opaque opt_typ_eq.
 
 (** Additionally, function definitions and function calls are annotated
   by function signatures indicating the number and types of arguments,
diff --git a/common/Memdata.v b/common/Memdata.v
index 8afe752..3de5f39 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -190,6 +190,7 @@ Opaque Byte.wordsize.
   replace (Zsucc (Z_of_nat n) * 8) with (Z_of_nat n * 8 + 8) by omega.
   rewrite two_p_is_exp; try omega. 
   rewrite Zmod_recombine. rewrite IHn. rewrite Zplus_comm. 
+  change (Byte.unsigned (Byte.repr x)) with (Byte.Z_mod_modulus x). 
   rewrite Byte.Z_mod_modulus_eq. reflexivity. 
   apply two_p_gt_ZERO. omega. apply two_p_gt_ZERO. omega.
 Qed.
diff --git a/common/Memory.v b/common/Memory.v
index bfaf67d..12a0f45 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -26,6 +26,7 @@
 - [free]: invalidate a memory block.
 *)
 
+Require Import Zwf.
 Require Import Axioms.
 Require Import Coqlib.
 Require Import Maps.
@@ -155,7 +156,7 @@ Remark perm_order_dec:
   forall p1 p2, {perm_order p1 p2} + {~perm_order p1 p2}.
 Proof.
   intros. destruct p1; destruct p2; (left; constructor) || (right; intro PO; inversion PO).
-Qed.
+Defined.
 
 Remark perm_order'_dec:
   forall op p, {perm_order' op p} + {~perm_order' op p}.
@@ -163,14 +164,14 @@ Proof.
   intros. destruct op; unfold perm_order'.
   apply perm_order_dec.
   right; tauto.
-Qed.
+Defined.
 
 Theorem perm_dec:
   forall m b ofs k p, {perm m b ofs k p} + {~ perm m b ofs k p}.
 Proof.
   unfold perm; intros.
   apply perm_order'_dec.
-Qed.
+Defined.
 
 Definition range_perm (m: mem) (b: block) (lo hi: Z) (k: perm_kind) (p: permission) : Prop :=
   forall ofs, lo <= ofs < hi -> perm m b ofs k p.
@@ -202,19 +203,15 @@ Lemma range_perm_dec:
   forall m b lo hi k p, {range_perm m b lo hi k p} + {~ range_perm m b lo hi k p}.
 Proof.
   intros. 
-  assert (forall n, 0 <= n ->
-          {range_perm m b lo (lo + n) k p} + {~ range_perm m b lo (lo + n) k p}).
-    apply natlike_rec2.
-    left. red; intros. omegaContradiction.
-    intros. destruct H0. 
-    destruct (perm_dec m b (lo + z) k p). 
-    left. red; intros. destruct (zeq ofs (lo + z)). congruence. apply r. omega. 
-    right; red; intro. elim n. apply H0. omega. 
-    right; red; intro. elim n. red; intros. apply H0. omega. 
+  induction lo using (well_founded_induction_type (Zwf_up_well_founded hi)).
   destruct (zlt lo hi).
-  replace hi with (lo + (hi - lo)) by omega. apply H. omega.
-  left; red; intros. omegaContradiction. 
-Qed.
+  destruct (perm_dec m b lo k p).
+  destruct (H (lo + 1)). red. omega. 
+  left; red; intros. destruct (zeq lo ofs). congruence. apply r. omega. 
+  right; red; intros. elim n. red; intros; apply H0; omega.
+  right; red; intros. elim n. apply H0. omega. 
+  left; red; intros. omegaContradiction.
+Defined.
 
 (** [valid_access m chunk b ofs p] holds if a memory access
     of the given chunk is possible in [m] at address [b, ofs]
@@ -289,7 +286,7 @@ Proof.
   left; constructor; auto.
   right; red; intro V; inv V; contradiction.
   right; red; intro V; inv V; contradiction.
-Qed.
+Defined.
 
 (** [valid_pointer m b ofs] returns [true] if the address [b, ofs]
   is nonempty in [m] and [false] if it is empty. *)
@@ -877,7 +874,7 @@ Proof.
   destruct (valid_access_dec m1 chunk b ofs Writable).
   eauto.
   contradiction.
-Qed.
+Defined.
 
 Hint Local Resolve valid_access_store: mem.
 
@@ -1363,7 +1360,7 @@ Proof.
   destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable).
   reflexivity. 
   contradiction.
-Qed.
+Defined.
 
 Theorem storebytes_store:
   forall m1 b ofs chunk v m2,
@@ -1774,7 +1771,7 @@ Theorem range_perm_free:
   { m2: mem | free m1 b lo hi = Some m2 }.
 Proof.
   intros; unfold free. rewrite pred_dec_true; auto. econstructor; eauto.
-Qed.
+Defined.
 
 Section FREE.
 
@@ -1949,7 +1946,7 @@ Theorem range_perm_drop_2:
 Proof.
   unfold drop_perm; intros. 
   destruct (range_perm_dec m b lo hi Cur Freeable). econstructor. eauto. contradiction.
-Qed.
+Defined.
 
 Section DROP.
 
diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v
index 860f04c..060d018 100644
--- a/ia32/Asmgenproof.v
+++ b/ia32/Asmgenproof.v
@@ -879,8 +879,8 @@ Opaque loadind.
   intros [m3' [P Q]].
   left; econstructor; split.
   apply plus_one. econstructor; eauto. 
-  subst x; simpl. eauto.
-Opaque Int.repr. 
+  subst x; simpl.
+  rewrite Int.unsigned_zero. simpl. eauto.
   simpl. rewrite C. simpl in F. rewrite (sp_val _ _ _ AG) in F. rewrite F.
   simpl in P. rewrite ATLR. rewrite P. eauto.
   econstructor; eauto.
diff --git a/ia32/Machregs.v b/ia32/Machregs.v
index 9935efa..df96393 100644
--- a/ia32/Machregs.v
+++ b/ia32/Machregs.v
@@ -40,7 +40,8 @@ Inductive mreg: Type :=
   | FT1: mreg (* X6 *) | FT2: mreg (* X7 *) | FP0: mreg (* top of FP stack *).
 
 Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}.
-Proof. decide equality. Qed.
+Proof. decide equality. Defined.
+Global Opaque mreg_eq.
 
 Definition mreg_type (r: mreg): typ :=
   match r with
diff --git a/ia32/Op.v b/ia32/Op.v
index 66ee633..a23e8ac 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -124,7 +124,7 @@ Proof.
   generalize Int.eq_dec; intro.
   assert (forall (x y: ident), {x=y}+{x<>y}). exact peq.
   decide equality.
-Qed.
+Defined.
 
 Definition eq_operation (x y: operation): {x=y} + {x<>y}.
 Proof.
@@ -135,7 +135,9 @@ Proof.
   assert (forall (x y: condition), {x=y}+{x<>y}). decide equality.
   decide equality.
   apply eq_addressing.
-Qed.
+Defined.
+
+Global Opaque eq_addressing eq_operation.
 
 (** * Evaluation functions *)
 
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 8aeadb9..f58a894 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -556,7 +556,8 @@ Proof.
   transitivity (p * (q / p)). omega. ring.
   right; red; intros. elim n. apply Z_div_exact_1; auto. 
   inv H0. rewrite Z_div_mult; auto. ring.
-Qed.
+Defined.
+Global Opaque Zdivide_dec.
 
 (** Conversion from [Z] to [nat]. *)
 
diff --git a/lib/Floats.v b/lib/Floats.v
index 63375ff..eb86027 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -854,6 +854,7 @@ Theorem floatofint_from_words:
     sub (from_words ox4330_0000 (Int.add x ox8000_0000))
         (from_words ox4330_0000 ox8000_0000).
 Proof.
+Local Transparent Int.repr Int64.repr.
   intros; destruct (Int.eq_dec x Int.zero); [subst; vm_compute; reflexivity|].
   assert (Int.signed x <> 0).
   intro; destruct n; rewrite <- (Int.repr_signed x), H; reflexivity.
diff --git a/lib/Integers.v b/lib/Integers.v
index 2c74e80..af9decd 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -227,7 +227,7 @@ Proof.
   intros. destruct x; destruct y. destruct (zeq intval0 intval1).
   left. apply mkint_eq. auto.
   right. red; intro. injection H. exact n.
-Qed.
+Defined.
 
 (** * Arithmetic and logical operations over machine integers *)
 
@@ -3711,4 +3711,4 @@ Module Int64 := Make(Wordsize_64).
 
 Notation int64 := Int64.int.
 
-
+Global Opaque Int.repr Int64.repr Byte.repr.
diff --git a/lib/Iteration.v b/lib/Iteration.v
index 1c3c9cc..f2e85ec 100644
--- a/lib/Iteration.v
+++ b/lib/Iteration.v
@@ -48,7 +48,7 @@ Hypothesis step_decr: forall a a', step a = inr _ a' -> ord a' a.
 Definition step_info (a: A) : {b | step a = inl _ b} + {a' | step a = inr _ a' & ord a' a}.
 Proof.
   caseEq (step a); intros. left; exists b; auto. right; exists a0; auto. 
-Qed.
+Defined.
 
 Definition iterate_F (a: A) (rec: forall a', ord a' a -> B) : B :=
   match step_info a with
diff --git a/lib/Maps.v b/lib/Maps.v
index 0c97ba5..a0287a4 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -32,6 +32,7 @@
   inefficient implementation of maps as functions is also provided.
 *)
 
+Require Import EquivDec.
 Require Import Coqlib.
 
 (* To avoid useless definitions of inductors in extracted code. *)
@@ -79,9 +80,6 @@ Module Type TREE.
   Hypothesis grspec:
     forall (A: Type) (i j: elt) (m: t A),
     get i (remove j m) = if elt_eq i j then None else get i m.
-  Hypothesis set2:
-    forall (A: Type) (i: elt) (m: t A) (v1 v2: A),
-    set i v2 (set i v1 m) = set i v2 m.
 
   (** Extensional equality between trees. *)
   Variable beq: forall (A: Type), (A -> A -> bool) -> t A -> t A -> bool.
@@ -144,17 +142,6 @@ Module Type TREE.
   Hypothesis elements_keys_norepet:
     forall (A: Type) (m: t A), 
     list_norepet (List.map (@fst elt A) (elements m)).
-  Hypothesis elements_canonical_order:
-    forall (A B: Type) (R: A -> B -> Prop) (m: t A) (n: t B),
-    (forall i x, get i m = Some x -> exists y, get i n = Some y /\ R x y) ->
-    (forall i y, get i n = Some y -> exists x, get i m = Some x /\ R x y) ->
-    list_forall2
-      (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y))
-      (elements m) (elements n).
-  Hypothesis elements_extensional:
-    forall (A: Type) (m n: t A),
-    (forall i, get i m = get i n) ->
-    elements m = elements n.
 
   (** Folding a function over all bindings of a tree. *)
   Variable fold:
@@ -200,8 +187,8 @@ Module PTree <: TREE.
 
   Inductive tree (A : Type) : Type :=
     | Leaf : tree A
-    | Node : tree A -> option A -> tree A -> tree A
-  .
+    | Node : tree A -> option A -> tree A -> tree A.
+
   Implicit Arguments Leaf [A].
   Implicit Arguments Node [A].
   Scheme tree_ind := Induction for tree Sort Prop.
@@ -378,15 +365,6 @@ Module PTree <: TREE.
     Variable A: Type.
     Variable eqA: A -> A -> Prop.
     Variable beqA: A -> A -> bool.
-    Hypothesis beqA_correct: forall x y, beqA x y = true -> eqA x y.
-
-    Definition exteq (m1 m2: t A) : Prop :=
-      forall (x: elt),
-      match get x m1, get x m2 with
-      | None, None => True
-      | Some y1, Some y2 => eqA y1 y2
-      | _, _ => False
-      end.
 
     Fixpoint bempty (m: t A) : bool :=
       match m with
@@ -395,15 +373,6 @@ Module PTree <: TREE.
       | Node l (Some _) r => false
       end.
 
-    Lemma bempty_correct:
-      forall m, bempty m = true -> forall x, get x m = None.
-    Proof.
-      induction m; simpl; intros. 
-      change (@Leaf A) with (empty A). apply gempty.
-      destruct o. congruence. destruct (andb_prop _ _ H). 
-      destruct x; simpl; auto.
-    Qed.
-
     Fixpoint beq (m1 m2: t A) {struct m1} : bool :=
       match m1, m2 with
       | Leaf, _ => bempty m2
@@ -417,6 +386,36 @@ Module PTree <: TREE.
           && beq l1 l2 && beq r1 r2
       end.
 
+    Lemma bempty_correct:
+      forall m, bempty m = true -> forall x, get x m = None.
+    Proof.
+      induction m; simpl; intros. 
+      change (@Leaf A) with (empty A). apply gempty.
+      destruct o. congruence. destruct (andb_prop _ _ H). 
+      destruct x; simpl; auto.
+    Qed.
+
+    Lemma bempty_complete:
+      forall m, (forall x, get x m = None) -> bempty m = true.
+    Proof.
+      induction m; simpl; intros.
+      auto.
+      destruct o. generalize (H xH); simpl; congruence.
+      rewrite IHm1. rewrite IHm2. auto. 
+      intros; apply (H (xI x)).
+      intros; apply (H (xO x)).
+    Qed.
+
+    Hypothesis beqA_correct: forall x y, beqA x y = true -> eqA x y.
+
+    Definition exteq (m1 m2: t A) : Prop :=
+      forall (x: elt),
+      match get x m1, get x m2 with
+      | None, None => True
+      | Some y1, Some y2 => eqA y1 y2
+      | _, _ => False
+      end.
+
     Lemma beq_correct:
       forall m1 m2, beq m1 m2 = true -> exteq m1 m2.
     Proof.
@@ -440,6 +439,25 @@ Module PTree <: TREE.
       auto.
     Qed.
 
+    Hypothesis beqA_complete: forall x y, eqA x y -> beqA x y = true.
+
+    Lemma beq_complete:
+      forall m1 m2, exteq m1 m2 -> beq m1 m2 = true.
+    Proof.
+      induction m1; destruct m2; simpl; intros. 
+      auto.
+      change (bempty (Node m2_1 o m2_2) = true).
+      apply bempty_complete. intros. generalize (H x). rewrite gleaf.
+      destruct (get x (Node m2_1 o m2_2)); tauto. 
+      change (bempty (Node m1_1 o m1_2) = true).
+      apply bempty_complete. intros. generalize (H x). rewrite gleaf.
+      destruct (get x (Node m1_1 o m1_2)); tauto.
+      apply andb_true_intro. split. apply andb_true_intro. split. 
+      generalize (H xH); simpl. destruct o; destruct o0; auto.
+      apply IHm1_1. red; intros. apply (H (xO x)). 
+      apply IHm1_2. red; intros. apply (H (xI x)). 
+    Qed.
+
   End EXTENSIONAL_EQUALITY.
 
     Fixpoint append (i j : positive) {struct i} : positive :=
diff --git a/lib/Ordered.v b/lib/Ordered.v
index ce1eca8..f52a7ef 100644
--- a/lib/Ordered.v
+++ b/lib/Ordered.v
@@ -42,7 +42,7 @@ Proof.
   apply EQ. red. apply Pos.compare_eq_iff. assumption.
   apply LT. assumption.
   apply GT. apply Pos.compare_gt_iff. assumption.
-Qed.
+Defined.
 
 Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := peq.
 
@@ -80,7 +80,7 @@ Proof.
   assert (Int.unsigned x <> Int.unsigned y).
     red; intros. rewrite <- (Int.repr_unsigned x) in n. rewrite <- (Int.repr_unsigned y) in n. congruence.
   red. omega.
-Qed.
+Defined.
 
 Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := Int.eq_dec.
 
@@ -118,14 +118,14 @@ Proof.
   apply LT. exact l. 
   apply EQ. red; red in e. apply A.index_inj; auto.
   apply GT. exact l.
-Qed.
+Defined.
 
 Lemma eq_dec : forall x y, { eq x y } + { ~ eq x y }.
 Proof.
   intros. case (peq (A.index x) (A.index y)); intros.
   left. apply A.index_inj; auto.
   right; red; unfold eq; intros; subst. congruence. 
-Qed.
+Defined.
 
 End OrderedIndexed.
 
@@ -208,7 +208,7 @@ Proof.
   apply EQ. red. tauto.
   apply GT. red. right. split. apply A.eq_sym. auto. auto.
   apply GT. red. left. auto.
-Qed.
+Defined.
 
 Lemma eq_dec : forall x y, { eq x y } + { ~ eq x y }.
 Proof.
@@ -218,7 +218,7 @@ Proof.
   left; auto.
   right; intuition.
   right; intuition.
-Qed.
+Defined.
 
 End OrderedPair.
 
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 7699fef..658653f 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -642,7 +642,6 @@ Opaque loadind.
   Simpl. rewrite <- H2. auto.
 
 - (* Mtailcall *)
-Opaque Int.repr.
   assert (f0 = f) by congruence.  subst f0.
   inversion AT; subst.
   assert (NOOV: list_length_z tf <= Int.max_unsigned).
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 1e16a0d..0e6d3e1 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -84,7 +84,7 @@ Proof.
   set (x := Int.sub n (low_s n)).
   assert (x = Int.add (Int.mul (Int.divu x (Int.repr 65536)) (Int.repr 65536))
                       (Int.modu x (Int.repr 65536))).
-    apply Int.modu_divu_Euclid. compute; congruence.
+    apply Int.modu_divu_Euclid. vm_compute; congruence.
   assert (Int.modu x (Int.repr 65536) = Int.zero).
     unfold Int.modu, Int.zero. decEq.
     change 0 with (0 mod 65536).
@@ -710,6 +710,7 @@ Proof.
   assert (Int.unsigned (Int.not i) <> Int.modulus - 1).
     red; intros.
     assert (Int.repr (Int.unsigned (Int.not i)) = Int.mone).
+Local Transparent Int.repr.
       rewrite H1. apply Int.mkint_eq. reflexivity. 
    rewrite Int.repr_unsigned in H2. 
    assert (Int.not (Int.not i) = Int.zero).
@@ -813,7 +814,7 @@ Lemma transl_op_correct_aux:
      match op with Omove => data_preg r = true | _ => nontemp_preg r = true end ->
      r <> preg_of res -> rs'#r = rs#r.
 Proof.
-Opaque Int.eq. Opaque Int.repr.
+Opaque Int.eq.
   intros. unfold transl_op in H; destruct op; ArgsInv; simpl in H0; try (inv H0); try TranslOpSimpl.
   (* Omove *)
   destruct (preg_of res) eqn:RES; destruct (preg_of m0) eqn:ARG; inv H.
diff --git a/powerpc/Op.v b/powerpc/Op.v
index a8936fe..110796b 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -120,14 +120,16 @@ Proof.
   assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality.
   assert (forall (x y: condition), {x=y}+{x<>y}). decide equality.
   decide equality.
-Qed.
+Defined.
 
 Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}.
 Proof.
   generalize Int.eq_dec; intro.
   assert (forall (x y: ident), {x=y}+{x<>y}). exact peq.
   decide equality.
-Qed.
+Defined.
+
+Global Opaque eq_addressing eq_operation.
 
 (** * Evaluation functions *)