aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Remove display .vo from default targetGravatar Jason Gross2017-03-06
* Fixes #127Gravatar jadep2017-03-06
* JavaDisplay depends on JavaNotations, not CNotationsGravatar Jason Gross2017-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...Gravatar 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
* make assert_preconditions way more sane; use vm_decide to kill most subgoalsGravatar jadep2017-03-02
* Separated out [carry] from other operations.Gravatar jadep2017-03-02
* Modify/add to NewBaseSystem to match with what is needed for proof of ring is...Gravatar jadep2017-03-01
* Fixed carry bugs (indexes need to be reversed, and we need to convert to/from...Gravatar jadep2017-03-01
* Defined [div] and [mod]; removed liftn_sig lemmas because they were actually ...Gravatar jadep2017-03-01
* Adjust implicits of flatten_binding_list_same_in_eqGravatar Jason Gross2017-03-01
* Add flatten_binding_list_In_eq_iff, flatten_binding_list_same_in_eqGravatar Jason Gross2017-03-01
* Add η principles for sigma typesGravatar Jason Gross2017-03-01
* Add dlet_nd notationGravatar Jason Gross2017-03-01
* Switch to fully uncurried form for reflectionGravatar Jason Gross2017-03-01
* Add interp_flat_type_rel_pointwise_SmartVarfMap, interp_flat_type_rel_pointwi...Gravatar Jason Gross2017-02-28
* Add SmartVarfMap Proper instanceGravatar Jason Gross2017-02-28
* Add strip_eta_tuple lemmasGravatar Jason Gross2017-02-28
* Better tuple_eta argumentsGravatar Jason Gross2017-02-28
* Add eta_tuple functionsGravatar Jason Gross2017-02-28
* Deduplicate codeGravatar Jason Gross2017-02-28
* Defined zero and one for NewBaseSystemGravatar jadep2017-02-27
* Added operation (including creating )Gravatar jadep2017-02-27
* Update _CoqProjectGravatar Jason Gross2017-02-27
* Added subtractionGravatar jadep2017-02-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 06:46:54 +0000