diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-10-11 16:39:13 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-10-11 16:39:13 +0100 |
| commit | f8bd8cde25321a3a4a3195bf9189416194b3732e (patch) | |
| tree | 7773d41eebb8ad6e26d545cc81ad51d24d2bd6a4 /src/hls/Array.v | |
| parent | c35404c110b7616b30eeb48fc4051dcb33d84f40 (diff) | |
| download | vericert-f8bd8cde25321a3a4a3195bf9189416194b3732e.tar.gz vericert-f8bd8cde25321a3a4a3195bf9189416194b3732e.zip | |
Clean up proofs
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), |