aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Expand)AuthorAge
* 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
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
* Switch to fully uncurried form for reflectionGravatar Jason Gross2017-03-01
* Update _CoqProjectGravatar Jason Gross2017-02-27
* speed up NewBaseystem synthesisGravatar Andres Erbsen2017-02-23
* Add BoundsInterpretationsGravatar Jason Gross2017-02-23
* Moved N lemmas from Ed25519 and IterAssocOp into new NUtil fileGravatar jadep2017-02-22
* Merge new base system (#112)Gravatar jadephilipoom2017-02-22
* Add various reflection improvements, boundbycastGravatar Jason Gross2017-02-21
* Add MapCastInterpGravatar Jason Gross2017-02-16
* Add InterpByIsoProofsGravatar Jason Gross2017-02-16
* Add InterpByIsoGravatar Jason Gross2017-02-16
* make update-_CoqProjectGravatar Jason Gross2017-02-15
* Add rudimentary Java and C notation files, displayGravatar Jason Gross2017-02-15
* Add partially finished MapCastWfGravatar Jason Gross2017-02-14
* Add src/Reflection/BoundByCastWf.vGravatar Jason Gross2017-02-14
* Add SmartBoundWfGravatar Jason Gross2017-02-14
* Add InlineCastInterp.vGravatar Jason Gross2017-02-13
* Add InlineCastWfGravatar Jason Gross2017-02-13
* Add SmartCast{Interp,Wf}Gravatar Jason Gross2017-02-13
* Split up BoundByCastGravatar Jason Gross2017-02-13
* Add EtaInterp, EtaWfGravatar Jason Gross2017-02-10
* Add Reflection/Eta.vGravatar Jason Gross2017-02-10
* Add files for constant reflective notationsGravatar Jason Gross2017-02-10
* added ZToRing to _CoqProjectGravatar jadep2017-02-09
* Factor things into BoundByCast.vGravatar Jason Gross2017-02-08
* Simpler version of MapCastGravatar Jason Gross2017-02-08
* Split up Reflection/Z/Syntax and make it smallerGravatar Jason Gross2017-02-02
* Add invert_opGravatar Jason Gross2017-02-01
* Add invert_exprGravatar Jason Gross2017-02-01
* Split off unique {pose,assert}Gravatar Jason Gross2017-01-31
* Add Util.SumboolGravatar Jason Gross2017-01-30
* Split off some bits of Reflection.SyntaxGravatar Jason Gross2017-01-26
* Update _CoqProjectGravatar Jason Gross2017-01-21
* Add LetInMonad to _CoqProjectGravatar Jason Gross2017-01-19
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 13:58:55 +0000