diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-11-13 14:32:32 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-11-13 14:32:32 +0100 |
| commit | 147fe13100aaacbd0906194f53a140373a7006d3 (patch) | |
| tree | 0b033dc1ffc44fc46937cccec5039537aa242e79 /lib/Integers.v | |
| parent | f2cf6d4e0600d4a58677a7531e8516a37fe1d0da (diff) | |
| parent | 40360396c621603af3ea6fb9a2fc89fa7945c79a (diff) | |
| download | compcert-kvx-147fe13100aaacbd0906194f53a140373a7006d3.tar.gz compcert-kvx-147fe13100aaacbd0906194f53a140373a7006d3.zip | |
Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge
Diffstat (limited to 'lib/Integers.v')
| -rw-r--r-- | lib/Integers.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index 3e78ee60..bc05a4da 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -3327,10 +3327,11 @@ Proof. assert (0 <= Z.min (size a) (size b)). generalize (size_range a) (size_range b). zify; omega. apply bits_size_3. auto. intros. - rewrite bits_and. zify. subst z z0. destruct H1. - rewrite (bits_size_2 a). auto. omega. - rewrite (bits_size_2 b). apply andb_false_r. omega. - omega. + rewrite bits_and by omega. + rewrite andb_false_iff. + generalize (bits_size_2 a i). + generalize (bits_size_2 b i). + zify; intuition. Qed. Corollary and_interval: |