diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-10-09 14:30:03 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-10-09 14:30:03 +0100 |
| commit | f06e5fc0ee651c3ffe357c3c3302ca1517381b4c (patch) | |
| tree | 15821bec5295bc84b95bd44b00e0d192c58c36fe /src/hls/Array.v | |
| parent | ce3adde4b50ba04430a1cf0ffb0ea85168091746 (diff) | |
| download | vericert-f06e5fc0ee651c3ffe357c3c3302ca1517381b4c.tar.gz vericert-f06e5fc0ee651c3ffe357c3c3302ca1517381b4c.zip | |
Fix warnings for Coq 8.13.2
Diffstat (limited to 'src/hls/Array.v')
| -rw-r--r-- | src/hls/Array.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/hls/Array.v b/src/hls/Array.v index dec1335..0f5ae02 100644 --- a/src/hls/Array.v +++ b/src/hls/Array.v @@ -51,7 +51,7 @@ Lemma list_set_spec1 {A : Type} : Proof. induction l; intros; destruct i; crush; firstorder. intuition. Qed. -Hint Resolve list_set_spec1 : array. +#[export] Hint Resolve list_set_spec1 : array. Lemma list_set_spec2 {A : Type} : forall l i (x : A) d, @@ -59,7 +59,7 @@ Lemma list_set_spec2 {A : Type} : Proof. induction l; intros; destruct i; crush; firstorder. intuition. Qed. -Hint Resolve list_set_spec2 : array. +#[export] Hint Resolve list_set_spec2 : array. Lemma list_set_spec3 {A : Type} : forall l i1 i2 (x : A), @@ -68,7 +68,7 @@ Lemma list_set_spec3 {A : Type} : Proof. induction l; intros; destruct i1; destruct i2; crush; firstorder. Qed. -Hint Resolve list_set_spec3 : array. +#[export] Hint Resolve list_set_spec3 : array. Lemma array_set_wf {A : Type} : forall l ln i (x : A), @@ -95,7 +95,7 @@ Proof. unfold array_set. crush. eauto with array. Qed. -Hint Resolve array_set_spec1 : array. +#[export] Hint Resolve array_set_spec1 : array. Lemma array_set_spec2 {A : Type} : forall a i (x : A) d, @@ -107,7 +107,7 @@ Proof. unfold array_set. crush. eauto with array. Qed. -Hint Resolve array_set_spec2 : array. +#[export] Hint Resolve array_set_spec2 : array. Lemma array_set_len {A : Type} : forall a i (x : A), |