aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Fix a name clashGravatar Jason Gross2017-03-14
* Add split_{m,o,}names_firstn_skipn and co.Gravatar Jason Gross2017-03-14
* Add firstn_skipnGravatar Jason Gross2017-03-14
* Add split_prodGravatar Jason Gross2017-03-14
* Add NameUtilPropertiesGravatar Jason Gross2017-03-14
* Add skipn_skipnGravatar Jason Gross2017-03-14
* Add InterpretToPHOASInterpGravatar Jason Gross2017-03-14
* Add Wf_InterpToPHOASGravatar Jason Gross2017-03-14
* Remove useless hypsGravatar Jason Gross2017-03-14
* Add InterpretToPHOASGravatar Jason Gross2017-03-14
* Move find_if_eq to Decidable.v, use Decidable in NamedGravatar Jason Gross2017-03-14
* Add ContextPropertiesGravatar Jason Gross2017-03-14
* Remove useless importsGravatar 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 faster versions of destruct_head_*Gravatar Jason Gross2017-03-14
* Fix more unfoldingGravatar Jason Gross2017-03-10
* Fix more unfolding that shouldn't happenGravatar Jason Gross2017-03-10
* Make sure interp_flat_type isn't unfolded in SmartMapGravatar Jason Gross2017-03-10
* Add better SmartFlatTypeMapInterp2Gravatar Jason Gross2017-03-08
* Remove interp_genf from Named/SyntaxGravatar Jason Gross2017-03-08
* Remove stuff from Reflection/Named/SyntaxGravatar Jason Gross2017-03-08
* Add FMapContext, PositiveContextGravatar Jason Gross2017-03-08
* Fixes #127Gravatar jadep2017-03-06
* Remove assert_preconditions; prove ring-ness of basesystem operations for bas...Gravatar jadep2017-03-04
* Separated out specific test cases for new base systemGravatar jadep2017-03-04
* Fixed admit left from fsatz portGravatar jadep2017-03-02
* make 8.5 happyGravatar Andres Erbsen2017-03-02
* fixup NewBasesystemGravatar Andres Erbsen2017-03-02
* remove dangling file that gives a warningGravatar Andres Erbsen2017-03-02
* remove undeclared lines from Ed25519Extraction.vGravatar Andres Erbsen2017-03-02
* move large non-building chunks of Ed25519.vGravatar Andres Erbsen2017-03-02
* deleted src/Specific/GF25519ExtendedAddCoordinates.vGravatar Andres Erbsen2017-03-02
* fix src/Specific/GF25519Reflective/Reified/AddCoordinates.vGravatar Andres Erbsen2017-03-02
* remove PointEncodingGravatar Andres Erbsen2017-03-02
* CompleteEdwardsCurveTheorems: point compressionGravatar Andres Erbsen2017-03-02
* PrimeFieldTheorems: inv for isomorphic fieldsGravatar Andres Erbsen2017-03-02
* use [positive] for [F] modulus, char_ge_C instead of char_gt_CGravatar Andres Erbsen2017-03-02
* rewrite ExtendedCoordinates, fix Ed25519Gravatar Andres Erbsen2017-03-02
* edwards curves over isomorphic fieldsGravatar Andres Erbsen2017-03-02
* src/Tactics/Algebra_syntax/Nsatz.v: power 1 onlyGravatar Andres Erbsen2017-03-02
* WIPGravatar Andres Erbsen2017-03-02
* address some code review commentsGravatar Andres Erbsen2017-03-02
* Weierstrass curve is a groupGravatar Andres Erbsen2017-03-02
* Attempt Weierstrass associativity again, good progress.Gravatar Andres Erbsen2017-03-02
* change weierstrass spec, prove most cases of associativityGravatar Andres Erbsen2017-03-02
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
* fsatz, nsatz_solve_nonzeroGravatar Andres Erbsen2017-03-02
* use field_nsatz in CompleteEdwardsCurve.PreGravatar Andres Erbsen2017-03-02
* field_nsatzGravatar Andres Erbsen2017-03-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-26 16:49:44 +0000