aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Expand)AuthorAge
...
* 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
* Move DemoWithReification.v => Experiments/SimplyTypedArithmetic.vGravatar Jason Gross2017-11-24
* Make a copy of Demo.vGravatar Jason Gross2017-11-24
* Add ModInv autosolverGravatar Jason Gross2017-11-16
* Update GeneralizeVar to ensure WfGravatar Jason Gross2017-11-13
* Make pipeline options more easily extensibleGravatar Jason Gross2017-11-13
* Add faster version of intros [a b] for reflective stuffGravatar Jason Gross2017-11-13
* Add autosolve admit packageGravatar Jason Gross2017-11-12
* automatic modifications to _Coqproject with new filesGravatar jadep2017-11-12
* Add Decidable2BoolGravatar Jason Gross2017-11-11
* Add ListUtil.ForallGravatar Jason Gross2017-11-11
* More modularity in autosolveGravatar Jason Gross2017-11-10
* Add HeadUnderBindersGravatar Jason Gross2017-11-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-28 19:20:51 +0000