Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | nsatz_contradict can now handle invalid _ <> _ hypotheses | 2016-06-23 | |
| | |||
* | Add Unit.v | 2016-06-23 | |
| | |||
* | Add equality on sum types | 2016-06-23 | |
| | |||
* | Merge pull request #8 from mit-plv/rsloan-pipeline-example-init | 2016-06-23 | |
|\ | | | | | Make Pipeline.v Build on 8.4 | ||
| * | Remove examples for 8.4 compatibility | 2016-06-23 | |
| | | |||
| * | Remove vestigal BoundedWord machinery | 2016-06-23 | |
| | | |||
* | | Improve some tactics and lemmas | 2016-06-23 | |
| | | |||
* | | [break_match] should not be local | 2016-06-23 | |
| | | |||
| * | Remove vestigal GaloisField machinery | 2016-06-23 | |
| | | |||
* | | Add tactics to Tactics, at most 2 sq-roots to Algebra | 2016-06-23 | |
| | | |||
| * | Make Pipeline.v Build on 8.4 | 2016-06-23 | |
|/ | |||
* | Merge pull request #7 from mit-plv/rsloan-unstable | 2016-06-23 | |
|\ | | | | | Merge Assembly Machinery into Master | ||
| * | Add Language.v, Conversion.v to _CoqProject | 2016-06-23 | |
| | | |||
* | | surjective homomorphism from group makes a group | 2016-06-23 | |
| | | |||
| * | Merge branch 'master' of github.com:mit-plv/fiat-crypto into ↵ | 2016-06-23 | |
| |\ | |/ |/| | | | public/rsloan-unstable | ||
| * | QhasmUtil.v: Remove 8.4-incompatible intro name | 2016-06-23 | |
| | | |||
| * | Pipeline: several new examples | 2016-06-23 | |
| | | |||
* | | Make [nsatz_contradict] better at inequalities | 2016-06-23 | |
| | | |||
| * | Pseudize Lemmas for Dual Operations | 2016-06-23 | |
| | | |||
* | | [field_algebra] now knows that 0 <> -0 is false | 2016-06-23 | |
| | | |||
* | | Work around bug #4851 in nsatz | 2016-06-23 | |
| | | | | | | | | | | Now our [nsatz] does not barf when you have duplicate equations in the context. | ||
* | | Add tactics for canonicalizing field (in)equalities | 2016-06-23 | |
| | | |||
* | | Rename the nonzero lemma to an iff lemma | 2016-06-23 | |
| | | |||
* | | Add mul_nonzero_nonzero_and to Algebra.v | 2016-06-23 | |
| | | |||
| * | Integrate Pseudize into Pipeline.v | 2016-06-23 | |
| | | |||
| * | Integrate Pseudize into Pipeline.v | 2016-06-23 | |
| | | |||
| * | Integrate Pseudize into Pipeline.v | 2016-06-23 | |
| | | |||
| * | Pseudize Let_In with minor notations | 2016-06-23 | |
| | | |||
| * | Pseudize Let_In | 2016-06-23 | |
| | | |||
| * | Add Pseudize, Vectorize, Wordize to the build process | 2016-06-22 | |
| | | |||
| * | Make Assembly modules 8.5-compatible | 2016-06-22 | |
| | | |||
| * | Merge with public master | 2016-06-22 | |
| |\ | |/ |/| | |||
* | | EdDSA.Notations: indentation | 2016-06-22 | |
| | | |||
* | | Fix broken notations (hopefully) | 2016-06-22 | |
| | | |||
* | | Fix missing notations | 2016-06-22 | |
| | | |||
* | | Aggregate all level specifications not in Spec/* | 2016-06-22 | |
| | | | | | | | | | | This prevents notation conflicts (see comment in Notations.v for more explanation). | ||
* | | Fix for broken abstract | 2016-06-22 | |
| | | | | | | | | It breaks when used in [Instance ... := _.] | ||
| * | Replace NPeano -> Nat in src/Spec/EdDSA | 2016-06-22 | |
| | | |||
* | | Add decidability util file | 2016-06-22 | |
| | | | | | | | | | | This will be useful for the Weierstrass curves, which require case-splitting on field equality. | ||
* | | Handle renaming of NPeano.pow to Nat.pow (#3) | 2016-06-22 | |
| | | | | | | | | We leave ambiguous which [pow] and [modulo] we refer to, so that this builds in both 8.4 and 8.5 | ||
| * | Merge with plv/master | 2016-06-22 | |
| |\ | |/ |/| | |||
| * | Merging Pipeline.v | 2016-06-22 | |
| |\ | |||
| * \ | squash commits + revert makefile | 2016-06-22 | |
| |\ \ | |||
| * | | | Fix build process | 2016-06-22 | |
| | | | | | | | | | | | | | | | | | | | | | | | | Fix build process Fix build process | ||
| * | | | Full automation for relevant parts of pseudo conversion except lets | 2016-06-22 | |
| | | | | |||
| * | | | Reorganization of wordize.v | 2016-06-22 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | first pseudo conversion lemma Decent machinery for automatic pseudo-conversion Decent machinery for automatic pseudo-conversion Decent machinery for automatic pseudo-conversion | ||
| * | | | Merging wordization and bounding together in Wordize.v | 2016-06-22 | |
| | | | | |||
| * | | | Really complex derivation of wand correctness | 2016-06-22 | |
| | | | | |||
| * | | | Proper word-based vectorization | 2016-06-22 | |
| | | | | | | | | | | | | | | | | | | | | | | | | Basic wordization lemmas Really complex derivation of wand correctness | ||
| * | | | ed25519: indentation fix | 2016-06-22 | |
| | | | |