aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Expand)AuthorAge
* 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
* Add aborted CompilePropertiesGravatar Jason Gross2017-03-22
* Add aborted MapCastByDeBruijnWfGravatar Jason Gross2017-03-19
* Add MapCastWfGravatar Jason Gross2017-03-19
* Most of the way towards a complete MapCastCorrectGravatar Jason Gross2017-03-19
* Add Named/PositiveContext/DefaultsProperties.vGravatar Jason Gross2017-03-19
* Split up ContextPropertiesGravatar Jason Gross2017-03-19
* Add IdContextGravatar Jason Gross2017-03-17
* Add MapCastByDeBruijn on PHOAS syntaxGravatar Jason Gross2017-03-17
* Add aborted in-process compile-{wf,interp} proofsGravatar Jason Gross2017-03-17
* Add a Named version of MapCastGravatar Jason Gross2017-03-17
* Add NameUtilPropertiesGravatar Jason Gross2017-03-14
* Add InterpretToPHOASInterpGravatar Jason Gross2017-03-14
* Add Wf_InterpToPHOASGravatar Jason Gross2017-03-14
* Add InterpretToPHOASGravatar Jason Gross2017-03-14
* Add ContextPropertiesGravatar Jason Gross2017-03-14
* Move ContextOk to ContextDefinitionsGravatar Jason Gross2017-03-14
* Add lemma about wff and interpf of NamedGravatar Jason Gross2017-03-14
* Add FMapContext, PositiveContextGravatar Jason Gross2017-03-08
* Separated out specific test cases for new base systemGravatar jadep2017-03-04
* remove dangling file...Gravatar Andres Erbsen2017-03-02
* deleted src/Specific/GF25519ExtendedAddCoordinates.vGravatar Andres Erbsen2017-03-02
* fix src/Specific/GF25519Reflective/Reified/AddCoordinates.vGravatar Andres Erbsen2017-03-02
* PrimeFieldTheorems: inv for isomorphic fieldsGravatar Andres Erbsen2017-03-02
* address some code review commentsGravatar Andres Erbsen2017-03-02
* Weierstrass curve is a groupGravatar Andres Erbsen2017-03-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-04 20:03:01 +0000