diff options
Diffstat (limited to 'src/hls/Array.v')
| -rw-r--r-- | src/hls/Array.v | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/hls/Array.v b/src/hls/Array.v index 5c7ebc7..dec1335 100644 --- a/src/hls/Array.v +++ b/src/hls/Array.v @@ -18,9 +18,11 @@ Set Implicit Arguments. -Require Import Lia. -Require Import Vericertlib. -From Coq Require Import Lists.List Datatypes. +Require Import Coq.Init.Datatypes. +Require Import Coq.Lists.List. +Require Import Coq.micromega.Lia. + +Require Import vericert.common.Vericertlib. Import ListNotations. @@ -74,7 +76,7 @@ Lemma array_set_wf {A : Type} : Proof. induction l; intros; destruct i; auto. - invert H; crush; auto. + invert H; crush. Qed. Definition array_set {A : Type} (i : nat) (x : A) (a : Array A) := |