aboutsummaryrefslogtreecommitdiff
path: root/src/Assembly
Commit message (Expand)AuthorAge
...
* More minor improvements in Conversions.v and Compile.vGravatar Robert Sloan2016-10-13
* Minor refactors waiting for the code generation to finishGravatar Robert Sloan2016-10-13
* Minor refactors waiting for the code generation to finishGravatar Robert Sloan2016-10-13
* Minor refactors waiting for the code generation to finishGravatar Robert Sloan2016-10-13
* Refactors of ge25519_ast working in Pipeline.vGravatar Rob Sloan2016-10-12
* Complete example + GF25519 outline in Pipeline.vGravatar Robert Sloan2016-10-02
* Most of our refactored compilation infrastructureGravatar Rob Sloan2016-10-02
* Fix merge with masterGravatar Robert Sloan2016-09-24
|\
* | Large-scale refactoring of src/AssemblyGravatar Robert Sloan2016-09-24
| * deduplicate Let_In into src/Util/LetIn.vGravatar Andres Erbsen2016-09-17
* | Finished more efficient WordRangeOptGravatar Robert Sloan2016-09-15
* | Most of a more efficient WordRangeOptGravatar Robert Sloan2016-09-13
| * Fully qualify [Require]sGravatar Jason Gross2016-09-08
* | Fix evalWordRangeOptGravatar Robert Sloan2016-08-26
* | Much tighter bounds in Evaluables.vGravatar Robert Sloan2016-08-26
* | Removed nat arguments to Evaluable operationsGravatar Robert Sloan2016-08-25
* | Finishing tactical machinery for bound-computingGravatar Robert Sloan2016-08-24
* | Experimental requirements for rsloan-phoasGravatar Robert Sloan2016-08-23
|/
* Remove unnecessary pseudo notations (#47)Gravatar Rob Sloan2016-08-08
* Move most notation level declarations into UtilGravatar Jason Gross2016-07-27
* Make the library 20% faster: [auto with *] is evilGravatar Jason Gross2016-07-22
* Remove examples for 8.4 compatibilityGravatar Robert Sloan2016-06-23
* Remove vestigal BoundedWord machineryGravatar Robert Sloan2016-06-23
* Make Pipeline.v Build on 8.4Gravatar Robert Sloan2016-06-23
* Add Language.v, Conversion.v to _CoqProjectGravatar Robert Sloan2016-06-23
* QhasmUtil.v: Remove 8.4-incompatible intro nameGravatar Robert Sloan2016-06-23
* Pipeline: several new examplesGravatar Robert Sloan2016-06-23
* Pseudize Lemmas for Dual OperationsGravatar Robert Sloan2016-06-23
* Integrate Pseudize into Pipeline.vGravatar Robert Sloan2016-06-23
* Integrate Pseudize into Pipeline.vGravatar Robert Sloan2016-06-23
* Pseudize Let_In with minor notationsGravatar Robert Sloan2016-06-23
* Pseudize Let_InGravatar Robert Sloan2016-06-23
* Add Pseudize, Vectorize, Wordize to the build processGravatar Robert Sloan2016-06-22
* Make Assembly modules 8.5-compatibleGravatar Robert Sloan2016-06-22
* Replace NPeano -> Nat in src/Spec/EdDSAGravatar Robert Sloan2016-06-22
* Fix build processGravatar Robert Sloan2016-06-22
* Full automation for relevant parts of pseudo conversion except letsGravatar Robert Sloan2016-06-22
* Decent machinery for automatic pseudo-conversionGravatar Robert Sloan2016-06-19
* Decent machinery for automatic pseudo-conversionGravatar Robert Sloan2016-06-19
* Decent machinery for automatic pseudo-conversionGravatar Robert Sloan2016-06-18
* first pseudo conversion lemmaGravatar Robert Sloan2016-06-14
* Reorganization of wordize.vGravatar Robert Sloan2016-06-14
* Merging wordization and bounding together in Wordize.vGravatar Robert Sloan2016-06-08
* Really complex derivation of wand correctnessGravatar Robert Sloan2016-06-07
* Really complex derivation of wand correctnessGravatar Robert Sloan2016-06-07
* Basic wordization lemmasGravatar Robert Sloan2016-06-06
* Proper word-based vectorizationGravatar Robert Sloan2016-06-06
* merging with masterGravatar Robert Sloan2016-06-06
|\
* | Full pipeline working againGravatar Robert Sloan2016-06-06
* | Huge Language / Conversion refactorsGravatar Robert Sloan2016-06-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 10:59:15 +0000