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

6 files changed, 12 insertions, 22 deletions

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 *)