diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-11-26 01:00:13 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-11-26 01:00:13 +0000 |
| commit | 29bee524cccfe08c680f655b1969a4c421e0a969 (patch) | |
| tree | 9a98159b31f566ad48712b7ada8bb6c25cf763c5 /src/hls/Array.v | |
| parent | d64f47def97420f40f61a53c385143b94b30b5b3 (diff) | |
| download | vericert-29bee524cccfe08c680f655b1969a4c421e0a969.tar.gz vericert-29bee524cccfe08c680f655b1969a4c421e0a969.zip | |
Fix build for Coq 8.12.1
Diffstat (limited to 'src/hls/Array.v')
| -rw-r--r-- | src/hls/Array.v | 6 |
1 files changed, 3 insertions, 3 deletions
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). |