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/Array.v     |  6 +++---
 src/hls/PrintHTL.ml |  1 -
 src/hls/Value.v     |  3 ++-
 src/hls/ValueInt.v  | 10 ----------
 src/hls/ValueVal.v  |  2 --
 5 files changed, 5 insertions(+), 17 deletions(-)

(limited to 'src/hls')

diff --git a/src/hls/Array.v b/src/hls/Array.v
index fe0f6b2..5eca269 100644
--- a/src/hls/Array.v
+++ b/src/hls/Array.v
@@ -29,7 +29,7 @@ Lemma list_set_spec1 {A : Type} :
   forall l i (x : A),
     i < length l -> nth_error (list_set i x l) i = Some x.
 Proof.
-  induction l; intros; destruct i; crush; firstorder.
+  induction l; intros; destruct i; crush; firstorder. intuition.
 Qed.
 Hint Resolve list_set_spec1 : array.
 
@@ -37,7 +37,7 @@ Lemma list_set_spec2 {A : Type} :
   forall l i (x : A) d,
     i < length l -> nth i (list_set i x l) d = x.
 Proof.
-  induction l; intros; destruct i; crush; firstorder.
+  induction l; intros; destruct i; crush; firstorder. intuition.
 Qed.
 Hint Resolve list_set_spec2 : array.
 
@@ -280,7 +280,7 @@ Proof.
   destruct i; crush.
 
   rewrite list_repeat_cons.
-  destruct i; crush; firstorder.
+  destruct i; crush; firstorder. intuition.
 Qed.
 
 Definition arr_repeat {A : Type} (a : A) (n : nat) : Array A := make_array (list_repeat a n).
diff --git a/src/hls/PrintHTL.ml b/src/hls/PrintHTL.ml
index 44f8b01..a75d0ee 100644
--- a/src/hls/PrintHTL.ml
+++ b/src/hls/PrintHTL.ml
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-open Value
 open Datatypes
 open Camlcoq
 open AST
diff --git a/src/hls/Value.v b/src/hls/Value.v
index d6a3d8b..0d3ea66 100644
--- a/src/hls/Value.v
+++ b/src/hls/Value.v
@@ -1,4 +1,4 @@
-(*
+(*(*
  * Vericert: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
@@ -549,3 +549,4 @@ Proof.
     apply Nat2Z.inj_lt in H2.
     assumption.
 Qed.
+*)
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',
diff --git a/src/hls/ValueVal.v b/src/hls/ValueVal.v
index b882dc6..96e0b1c 100644
--- a/src/hls/ValueVal.v
+++ b/src/hls/ValueVal.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 Export lib.Integers common.Values.
 From vericert Require Import Vericertlib.
-- 
cgit