diff options
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 de74611..8b7d262 100644 --- a/src/hls/Array.v +++ b/src/hls/Array.v @@ -76,7 +76,7 @@ Lemma array_set_wf {A : Type} : Proof. induction l; intros; destruct i; auto. - invert H; crush. + inv H; crush. Qed. Definition array_set {A : Type} (i : nat) (x : A) (a : Array A) := @@ -272,10 +272,10 @@ Proof. (* This is actually a degenerate case, not an unprovable goal. *) pose proof (in_app_or (list_repeat' [] a n) ([a])). - apply H0 in H. invert H. + apply H0 in H. inv H. - eapply IHn in X; eassumption. - - invert H1; contradiction. + - inv H1; contradiction. Qed. Lemma list_repeat_head_tail {A : Type} : forall n (a : A), |