From f178e5ba32761135cf433d7298624ff35ae44f44 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 21 Jan 2017 18:51:47 -0500
Subject: Revert "Fix a missing qualification"

This reverts commit 3c4ff8fe8d2154addcf440690d315c58a529c1f6.

Revert "Move weqb_hetero to Bedrock.Word"

This reverts commit c83cb07f1477de33ce9eb43eea6a4f2720a94763.

We probably shouldn't modify Bedrock.Word
---
 Bedrock/Word.v      | 10 ----------
 src/Util/WordUtil.v | 52 ++++++++++++++++++++++++++++++++--------------------
 2 files changed, 32 insertions(+), 30 deletions(-)

diff --git a/Bedrock/Word.v b/Bedrock/Word.v
index 10bd452bb..2c518807d 100644
--- a/Bedrock/Word.v
+++ b/Bedrock/Word.v
@@ -300,16 +300,6 @@ Definition weq : forall sz (x y : word sz), {x = y} + {x <> y}.
   abstract (rewrite (shatter_word y); simpl; intro; injection H; auto).
 Defined.
 
-Fixpoint weqb_hetero sz1 sz2 (x : word sz1) (y : word sz2) : bool :=
-  match x, y with
-  | WO, WO => true
-  | WO, _ => false
-  | WS b _ x', WS b' _ y'
-    => eqb b b' && @weqb_hetero _ _ x' y'
-  | WS _ _ _, _
-    => false
-  end%bool.
-Global Arguments weqb_hetero {_ _} _ _.
 Fixpoint weqb sz (x : word sz) : word sz -> bool :=
   match x in word sz return word sz -> bool with
     | WO => fun _ => true
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 0e3f6a168..7f8d7b824 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -22,6 +22,38 @@ Create HintDb push_wordToN discriminated.
 Hint Extern 1 => autorewrite with pull_wordToN in * : pull_wordToN.
 Hint Extern 1 => autorewrite with push_wordToN in * : push_wordToN.
 
+Module Word.
+  Fixpoint weqb_hetero sz1 sz2 (x : word sz1) (y : word sz2) : bool :=
+    match x, y with
+    | WO, WO => true
+    | WO, _ => false
+    | WS b _ x', WS b' _ y'
+      => eqb b b' && @weqb_hetero _ _ x' y'
+    | WS _ _ _, _
+      => false
+    end%bool.
+  Global Arguments weqb_hetero {_ _} _ _.
+  Theorem weqb_hetero_true_iff : forall sz1 x sz2 y,
+      @weqb_hetero sz1 sz2 x y = true <-> exists pf : sz1 = sz2, eq_rect _ word x _ pf = y.
+  Proof.
+    induction x; intros sz2 y; (split; [ destruct y | ]);
+      repeat first [ progress simpl
+                   | intro
+                   | congruence
+                   | exists eq_refl
+                   | progress destruct_head ex
+                   | progress destruct_head bool
+                   | progress subst
+                   | progress split_andb
+                   | match goal with
+                     | [ IHx : forall sz2 y, weqb_hetero _ y = true <-> _, H : weqb_hetero _ _ = true |- _ ]
+                       => apply IHx in H
+                     | [ IHx : forall sz2 y, weqb_hetero _ y = true <-> _ |- weqb_hetero ?x ?x = true ]
+                       => apply IHx
+                     end ].
+  Qed.
+End Word.
+
 (* Utility Tactics *)
 
 Ltac word_util_arith := omega.
@@ -1212,23 +1244,3 @@ Lemma wlast_combine : forall sz a b, @wlast sz (combine a (WS b WO)) = b.
 Proof.
   intros; unfold wlast; rewrite split2_combine; cbv; reflexivity.
 Qed.
-
-Theorem weqb_hetero_true_iff : forall sz1 x sz2 y,
-    @weqb_hetero sz1 sz2 x y = true <-> exists pf : sz1 = sz2, eq_rect _ word x _ pf = y.
-Proof.
-  induction x; intros sz2 y; (split; [ destruct y | ]);
-    repeat first [ progress simpl
-                 | intro
-                 | congruence
-                 | exists Logic.eq_refl
-                 | progress destruct_head ex
-                 | progress destruct_head bool
-                 | progress subst
-                 | progress split_andb
-                 | match goal with
-                   | [ IHx : forall sz2 y, weqb_hetero _ y = true <-> _, H : weqb_hetero _ _ = true |- _ ]
-                     => apply IHx in H
-                   | [ IHx : forall sz2 y, weqb_hetero _ y = true <-> _ |- weqb_hetero ?x ?x = true ]
-                     => apply IHx
-                   end ].
-Qed.
-- 
cgit v1.2.3