aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Expand)AuthorAge
* Add PrimitiveSigmaGravatar Jason Gross2018-09-14
* Add a rudimentary arg parse moduleGravatar Jason Gross2018-08-30
* Add src/Util/PER.vGravatar Jason Gross2018-08-29
* Minor improvements to various ZUtil things; boundsGravatar Jason Gross2018-08-25
* Bump bbvGravatar Jason Gross2018-08-24
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* Add more operation-specific proofsGravatar Jason Gross2018-08-21
* Add the file proving split_bounds correctGravatar Jason Gross2018-08-13
* Split up rewrite rules proofs into multiple filesGravatar Jason Gross2018-08-13
* Start setting up abs-int interp proofsGravatar Jason Gross2018-08-06
* Add related_iff_app_curriedGravatar Jason Gross2018-08-06
* Add GENERATEDIdentifiersWithoutTypesProofs.vGravatar Jason Gross2018-08-02
* Integrate Wf and Interp proofsGravatar Jason Gross2018-07-30
* Add Wf proofs about MiscCompilerPassesGravatar Jason Gross2018-07-26
* Add Wf lemmas about SubstVarGravatar Jason Gross2018-07-26
* Add basic wf proofsGravatar Jason Gross2018-07-26
* Add some inversion lemmas and tacticsGravatar Jason Gross2018-07-25
* Montgomery reduction in new pipelineGravatar Jason Gross2018-07-21
* Make Z.div_mod_to_quot_rem strongerGravatar Jason Gross2018-07-10
* Shuffle some ZUtil lemmas aroundGravatar Jason Gross2018-07-08
* Add ZUtil.SortingGravatar Jason Gross2018-06-29
* Add specialize_all_ways, fix a proof in src/Compilers/Z/ArithmeticSimplifierI...Gravatar Jason Gross2018-06-26
* New pipeline, split among filesGravatar Jason Gross2018-06-17
* Add ErrorT monad, and Show classGravatar Jason Gross2018-06-15
* Add PrimitiveHList, PrimitiveProdGravatar Jason Gross2018-06-13
* Move Option.List.map to OptionList.map to fix name clashes in TupleGravatar Jason Gross2018-06-04
* make update-_CoqProjectGravatar Jason Gross2018-05-05
* Merge pull request #335 from mit-plv/cpsloopsGravatar Andres Erbsen2018-04-18
|\
* | Add new assembly-mimicking operations rshi, cc_m, and cc_lGravatar Jade Philipoom2018-04-11
* | Update number/string conversionsGravatar Jason Gross2018-04-09
| * move Loops from Experiments to UtilGravatar Andres Erbsen2018-03-27
| * remove old loops codeGravatar Andres Erbsen2018-03-27
|/
* Add Algebra.SubsetoidRingGravatar Jason Gross2018-03-12
* make update-_CoqProjectGravatar Jason Gross2018-03-10
* Prove another Barrett reduction variant.Gravatar David Benjamin2018-03-09
* Add new modular addition operation on ZGravatar Jade Philipoom2018-02-23
* Add pointed typesGravatar Jason Gross2018-02-18
* Add a file to parse taps with Coq notationsGravatar Jason Gross2018-02-14
* Add some string utility functionsGravatar Jason Gross2018-02-13
* Add string conversionsGravatar Jason Gross2018-02-11
* Split off ZRange lemmasGravatar Jason Gross2018-02-10
* Add some ZRange operationsGravatar Jason Gross2018-02-10
* minor updates needed to make it compile with bbvGravatar Samuel Gruetter2018-02-05
* add bedrock bit vectors library (bbv) as a submodule replacing the Bedrock di...Gravatar Samuel Gruetter2018-02-05
* Add x25519 donna versions with the new way of generating C codeGravatar Jason Gross2018-01-15
* Generate fecarry for solinasGravatar Jason Gross2018-01-10
* Factor out fsatz lemmasGravatar Jason Gross2018-01-09
* @davidben merged Jacobian+affine into Jacobian+JacobianGravatar Andres Erbsen2018-01-09
* Jacobian coordinatesGravatar Andres Erbsen2018-01-09
* Add Tactics.RunTacticAsConstrGravatar Jason Gross2017-11-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-28 15:54:32 +0000