diff options
| author |  Robert Sloan <varomodt@gmail.com> | 2016-06-14 21:21:47 -0400 |
|---|---|---|
| committer | Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:45:18 -0400 |
| commit | 1481b88f0c2498f41421c1333856e4458b186618 (patch) | |
| tree | f8b6267aba7c7e30e57f3c19df1e79c3b8ab4f6e /src/Assembly/Vectorize.v | |
| parent | 2c4a10de8bde2986d7f32598d9e6be7fb84cb7bc (diff) | |
Reorganization of wordize.v
first pseudo conversion lemma
Decent machinery for automatic pseudo-conversion
Decent machinery for automatic pseudo-conversion
Decent machinery for automatic pseudo-conversion
Diffstat (limited to 'src/Assembly/Vectorize.v')
| -rw-r--r-- | src/Assembly/Vectorize.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/Assembly/Vectorize.v b/src/Assembly/Vectorize.v index 71d4d573d..f8139bf92 100644 --- a/src/Assembly/Vectorize.v +++ b/src/Assembly/Vectorize.v @@ -1,4 +1,3 @@ - Require Export Bedrock.Word Bedrock.Nomega. Require Import NPeano NArith PArith Ndigits Compare_dec Arith. Require Import ProofIrrelevance Ring List. |