aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Expand)AuthorAge
* Add CSE correctness files for Z-specializationGravatar Jason Gross2017-04-15
* Remove old versions of wordsize selectionGravatar Jason Gross2017-04-14
* Add CSE specialized to ZGravatar Jason Gross2017-04-14
* Add some CSE propertiesGravatar Jason Gross2017-04-14
* Add test for squareGravatar Jason Gross2017-04-14
* Add for-loop combinatorGravatar Jason Gross2017-04-14
* Prove interp correctness of register reassignGravatar Jason Gross2017-04-13
* Add Util.Logic.ImplAndGravatar Jason Gross2017-04-13
* Add denoter for symbolic_exprGravatar Jason Gross2017-04-12
* Add initial version of CSE interpGravatar Jason Gross2017-04-11
* Finish most of wf for CSEGravatar Jason Gross2017-04-10
* Add AListContext, WeakListContextGravatar Jason Gross2017-04-10
* Split off Compilers.Named.ContextGravatar Jason Gross2017-04-10
* Split off ZUtil.Stabilization, finish IsBoundedBy!Gravatar Jason Gross2017-04-09
* Split up Compilers/Z/Bounds/InterpretationLemmasGravatar Jason Gross2017-04-07
* Parameterize bounds analysis over round_upGravatar Jason Gross2017-04-07
* Add display for ladderstep 130-bitGravatar Jason Gross2017-04-07
* Add 130-bit 3-register synthesisGravatar Jason Gross2017-04-07
* Add Display files and targetsGravatar Jason Gross2017-04-07
* Add IntegrationTestLadderstep.vGravatar Jason Gross2017-04-07
* make update-_CoqProjectGravatar Jason Gross2017-04-07
* Merge branch 'rename-everything'. Closes #14.Gravatar Andres Erbsen2017-04-06
|\
| * rename-everythingGravatar Andres Erbsen2017-04-06
| * remove unused filesGravatar Andres Erbsen2017-04-06
* | Add IntegrationTest for SubGravatar Jason Gross2017-04-06
* | Rename IntegrationTest{=>Mul}.vGravatar Jason Gross2017-04-06
| * start removing BaseSystemGravatar Andres Erbsen2017-04-06
| * git rm -rf src/BoundedArithmetic/Double/Repeated/ (and users)Gravatar Andres Erbsen2017-04-06
| * remove Encoding stuffGravatar Andres Erbsen2017-04-06
| * git rm -rf src/AssemblyGravatar Andres Erbsen2017-04-06
|/
* Add clear_allGravatar Jason Gross2017-04-06
* Support Z.oppGravatar Jason Gross2017-04-05
* make elliptic curve proofs faster and split them into filesGravatar Andres Erbsen2017-04-05
* Add TransparentAssertGravatar Jason Gross2017-04-05
* Actually add ChangeInAllGravatar Jason Gross2017-04-05
* Add Tactics.ChangeInAllGravatar Jason Gross2017-04-05
* Add Tactics.MoveLetInGravatar Jason Gross2017-04-05
* Add Tactics.PrintContextGravatar Jason Gross2017-04-04
* Move sigma MapProjections to a separate fileGravatar Jason Gross2017-04-04
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
* Split off liftn_sig, add lift{3,4}_sigGravatar Jason Gross2017-04-03
* make update-_CoqProjectGravatar Jason Gross2017-04-03
* Add an initial stab at doing the pipeline mostly in GallinaGravatar Jason Gross2017-04-03
* Rename PreDefinitions to OutputTypeGravatar Jason Gross2017-04-03
* An approximately first stab DeBruijn word-size-selGravatar Jason Gross2017-04-03
* Remove old reflective pipeline, making way the newGravatar Jason Gross2017-04-03
* Remove everything after the individual reified opsGravatar Jason Gross2017-04-03
* Add UnifyAbstractReflexivity tacticsGravatar Jason Gross2017-04-03
* Add Tactics.EvarExistsGravatar Jason Gross2017-04-02
* Add Util.SigmaAssocGravatar Jason Gross2017-04-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 13:20:03 +0000