aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Expand)AuthorAge
...
* | 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
* Remove the bits of the new reflective pipeline in masterGravatar Jason Gross2017-04-02
* Remove all the .v files in SpecificGenGravatar Jason Gross2017-04-02
* Add PreDefinitions pipeline fileGravatar Jason Gross2017-04-02
* Add Z instantiations of InlineConstGravatar Jason Gross2017-04-02
* Add Z.Bounds.MapCastByDeBruijn instantiationGravatar Jason Gross2017-04-02
* Add Z instantiation of MapCastByDeBruijnInterpGravatar Jason Gross2017-04-02
* Add an initial glue file in the pipeline, no option in boundsGravatar Jason Gross2017-04-01
* Split off BoundedWord.v from IntegrationTest.vGravatar Jason Gross2017-04-01
* Add RenameBindersGravatar Jason Gross2017-04-01
* Add wf proof for arithmetic simpliferGravatar Jason Gross2017-04-01
* Add an arithmetic simplifierGravatar Jason Gross2017-04-01
* Add correctness of RewriterGravatar Jason Gross2017-04-01
* Add Reflection/Rewriter.vGravatar Jason Gross2017-04-01
* Split out Tactics.SubstLetGravatar Jason Gross2017-04-01
* Add a bounds relaxation lemmaGravatar Jason Gross2017-03-31
* Add [etransitivity y], [etransitivity_rev] tacticsGravatar Jason Gross2017-03-31
* use improved fsatz on various elliptic curve thingsGravatar Andres Erbsen2017-03-31
* Start instantiating MapCastByDeBruijn in Z/Gravatar Jason Gross2017-03-30
* Don't linearize and eta in MapCastByDeBruijnGravatar Jason Gross2017-03-30
* Rename Bounds to ZRange, use Prop, not boolGravatar Jason Gross2017-03-30
* Add a file dedicated to the definition of Z boundsGravatar Jason Gross2017-03-30
* Add Z.FoldTypes.{Min,Max}TypeUsedGravatar Jason Gross2017-03-28
* Add FoldTypesGravatar Jason Gross2017-03-28
* make update-_CoqProjectGravatar Jason Gross2017-03-28
* Added saturated arithmetic file, including [compact] code and proofGravatar jadep2017-03-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 03:05:47 +0000