diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-01-21 22:18:50 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-21 22:18:50 +0000 |
| commit | 3addff470c8faeb6876c63575184caa0aa829e28 (patch) | |
| tree | 84684245fd8e57b96b28ed4f486242c5bc3e0732 /src/hls/Array.v | |
| parent | ff4257c78aeefee69f3b17702153296c8c639348 (diff) | |
| download | vericert-3addff470c8faeb6876c63575184caa0aa829e28.tar.gz vericert-3addff470c8faeb6876c63575184caa0aa829e28.zip | |
Fix imports in Coq modules
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) := |