aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Update makefile and Coq dependencies with CompCertYann Herklotz2020-02-143-2/+10
* Add nix dependenciesYann Herklotz2020-02-141-1/+2
* Add project files and compcert interconnectYann Herklotz2020-02-144-0/+98
* Add CompCert as a libraryYann Herklotz2020-02-132-0/+3
* Improve the Coq sources and add extractionYann Herklotz2020-02-135-53/+45
* Add dune files to .gitignoreYann Herklotz2020-02-041-1/+6
* Add ExtractionYann Herklotz2020-02-043-13/+19
* Add show typeclassYann Herklotz2020-02-041-0/+42
* Add main.ml fileYann Herklotz2020-02-042-0/+12
* Add extraction to gitignoreYann Herklotz2020-02-041-0/+2
* Add extractionYann Herklotz2020-02-041-0/+4
* Add installYann Herklotz2020-02-041-1/+6
* Add nix fileYann Herklotz2020-02-042-2/+23
* Short proof and add TacticsYann Herklotz2020-01-292-12/+31
* Proof of nat_to_value_is_flat addedYann Herklotz2020-01-291-29/+28
* Trying some more proofsYann Herklotz2020-01-241-7/+50
* Added value_to_natYann Herklotz2020-01-243-18/+31
* Reorder to let it compile againYann Herklotz2020-01-241-37/+35
* Finish some proofs and convert to natYann Herklotz2020-01-241-12/+16
* Add some proofs about valuesYann Herklotz2020-01-232-95/+181
* Remove bbvYann Herklotz2020-01-232-3/+0
* Fix project linksYann Herklotz2020-01-221-2/+2
* Move into src directoryYann Herklotz2020-01-223-0/+0
* Add helper function for 'optional'Yann Herklotz2020-01-221-0/+10
* Add initial implementations for evaluationYann Herklotz2020-01-221-7/+34
* Include library in the projectYann Herklotz2020-01-221-0/+1
* Add bbv libraryYann Herklotz2020-01-222-0/+3
* Add Verilog syntaxYann Herklotz2020-01-212-0/+81
* Update Makefile and gitignoreYann Herklotz2019-11-042-7/+11
* Add Args change to MakefileYann Herklotz2019-11-041-1/+1
* Add initial Coq fileYann Herklotz2019-11-041-0/+1
* Add Makefile and _CoqProjectYann Herklotz2019-11-042-0/+23
* Initial commitYann Herklotz2019-10-023-0/+53