diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-07-08 14:43:57 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-07-08 14:43:57 +0200 |
| commit | e73d5db97cdb22cce2ee479469f62af3c4b6264a (patch) | |
| tree | 035d31018c2abec698eb49a205c60bbf5c24ba0d /lib/Integers.v | |
| parent | db2445b3b745abd1a26f5a832a29ca269c725277 (diff) | |
| download | compcert-kvx-e73d5db97cdb22cce2ee479469f62af3c4b6264a.tar.gz compcert-kvx-e73d5db97cdb22cce2ee479469f62af3c4b6264a.zip | |
Port to Coq 8.5pl2
Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.
Diffstat (limited to 'lib/Integers.v')
| -rw-r--r-- | lib/Integers.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index a0140e57..316dfb52 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -53,7 +53,7 @@ Definition swap_comparison (c: comparison): comparison := (** * Parameterization by the word size, in bits. *) Module Type WORDSIZE. - Variable wordsize: nat. + Parameter wordsize: nat. Axiom wordsize_not_zero: wordsize <> 0%nat. End WORDSIZE. @@ -3378,7 +3378,7 @@ Proof. repeat rewrite unsigned_repr. tauto. generalize wordsize_max_unsigned; omega. generalize wordsize_max_unsigned; omega. - intros. unfold one_bits in H. + unfold one_bits. intros. destruct (list_in_map_inv _ _ _ H) as [i0 [EQ IN]]. subst i. apply A. apply Z_one_bits_range with (unsigned x); auto. Qed. @@ -3576,8 +3576,8 @@ Proof. intros. destruct (andb_prop _ _ H1). clear H1. destruct (andb_prop _ _ H2). clear H2. - exploit proj_sumbool_true. eexact H1. intro A; clear H1. - exploit proj_sumbool_true. eexact H4. intro B; clear H4. + apply proj_sumbool_true in H1. + apply proj_sumbool_true in H4. assert (unsigned ofs1 + sz1 <= unsigned ofs2 \/ unsigned ofs2 + sz2 <= unsigned ofs1). destruct (orb_prop _ _ H3). left. eapply proj_sumbool_true; eauto. right. eapply proj_sumbool_true; eauto. clear H3. |