From 29bee524cccfe08c680f655b1969a4c421e0a969 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 26 Nov 2020 01:00:13 +0000
Subject: Fix build for Coq 8.12.1

---
 src/hls/ValueInt.v | 10 ----------
 1 file changed, 10 deletions(-)

(limited to 'src/hls/ValueInt.v')

diff --git a/src/hls/ValueInt.v b/src/hls/ValueInt.v
index f1fd056..e434abc 100644
--- a/src/hls/ValueInt.v
+++ b/src/hls/ValueInt.v
@@ -17,8 +17,6 @@
  *)
 
 (* begin hide *)
-From bbv Require Import Word.
-From bbv Require HexNotation WordScope.
 From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia.
 From compcert Require Import lib.Integers common.Values.
 From vericert Require Import Vericertlib.
@@ -98,14 +96,6 @@ Definition boolToValue (b : bool) : value :=
 
 (** ** Arithmetic operations *)
 
-Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1.
-intros; subst; assumption. Defined.
-
-Lemma unify_word_unfold :
-  forall sz w,
-  unify_word sz sz w eq_refl = w.
-Proof. auto. Qed.
-
 Inductive val_value_lessdef: val -> value -> Prop :=
 | val_value_lessdef_int:
     forall i v',
-- 
cgit