1 files changed, 6 insertions, 40 deletions

diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
index 83ef5b701..b12e27e19 100644
--- a/src/Assembly/QhasmEvalCommon.v
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -1,7 +1,7 @@
 Require Export QhasmCommon QhasmUtil State.
 Require Export ZArith Sumbool.
 Require Export Bedrock.Word.
-Require Import Logic.Eqdep_dec.
+Require Import Logic.Eqdep_dec ProofIrrelevance.
 
 Import Util.
 
@@ -116,12 +116,11 @@ Module EvalUtil.
         then left _
         else right _
 
-    | (memM _ v, memM _ v') => fun _ => 
+    | (memM _ v i, memM _ v' i') => fun _ => 
         if (Nat.eq_dec (memName v) (memName v')) 
         then if (Nat.eq_dec (memLength v) (memLength v'))
-        then left _
-        else right _
-        else right _
+        then if (Nat.eq_dec (proj1_sig i) (proj1_sig i'))
+        then left _ else right _ else right _ else right _
 
     | _ => fun _ => right _
     end (eq_refl (a, b))); abstract (
@@ -137,6 +136,8 @@ Module EvalUtil.
           rewrite _H0
         | apply (inj_pair2_eq_dec _ Nat.eq_dec) in H3
         | inversion H; subst; intuition
+        | destruct i, i'; simpl in _H2; subst;
+          replace l with l0 by apply proof_irrelevance
         | intuition ]).
   Defined.
 
@@ -170,41 +171,6 @@ Module EvalUtil.
       end
     end.
 
-    (* Mapping Identifier-Triples *)
-
-  Definition mappingId {n} (x: Mapping n): nat * nat * nat :=
-    match x with
-    | regM (reg n _ v) => (0, n, v)
-    | stackM (stack n _ v) => (1, n, v)
-    | constM (const n _ w) => (2, n, wordToNat w)
-    | memM _ (mem n m _ v) => (3, m, v)
-    end.
-
-  Lemma id_equal: forall {n: nat} (x y: Mapping n),
-    x = y <-> mappingId x = mappingId y.
-  Proof.
-    intros; split; intros; try abstract (rewrite H; intuition);
-      destruct x as [x | x | x | x], y as [y | y | y | y];
-      destruct x, y; unfold mappingId in H; simpl in H;
-
-      repeat match goal with
-      | [X: (_, _, _) = (_, _, _) |- _ ] =>
-        apply Triple_as_OT.conv in X
-      | [X: _ /\ _ /\ _ |- _ ] => destruct X
-      | [X: _ /\ _ |- _ ] => destruct X
-      | [A: Width _, B: Width _ |- _ ] =>
-        replace A with B by (apply width_eq)
-      | [X: context[match ?a with | _ => _ end] |- _ ] =>
-        destruct a
-      end; try subst; try omega; intuition.
-
-    rewrite <- (natToWord_wordToNat w0);
-      rewrite <- (natToWord_wordToNat w2);
-      rewrite H1; intuition.
-  Qed.
-
-  Definition id_dec := Triple_as_OT.eq_dec.
-
 End EvalUtil.
 
 Module QhasmEval.