aboutsummaryrefslogtreecommitdiff
path: root/src/Specific
Commit message (Expand)AuthorAge
* Remove the bits of the new reflective pipeline in masterGravatar Jason Gross2017-04-02
* Add an initial glue file in the pipeline, no option in boundsGravatar Jason Gross2017-04-01
* Fix definition of BoundedWordGravatar Jason Gross2017-04-01
* Split off BoundedWord.v from IntegrationTest.vGravatar Jason Gross2017-04-01
* insert a reduce step in the correct place of the carry chainGravatar jadep2017-04-01
* Add a comment explaining bounds_expGravatar Jason Gross2017-03-30
* Update IntegrationTest with actual boundsGravatar Jason Gross2017-03-30
* Created test file for newbasesystem/word-size-selection integrationGravatar jadep2017-03-30
* turn [Let]s into [Definition]s so they persist after the sectionGravatar jadep2017-03-30
* change import order to avoid name-clash with [List.repeat] and [Tuple.repeat]Gravatar jadep2017-03-30
* Get rid of list-based Tuple.mapGravatar Jason Gross2017-03-30
* Add Wf_InterpToPHOASGravatar Jason Gross2017-03-14
* Move ContextOk to ContextDefinitionsGravatar Jason Gross2017-03-14
* Remove stuff from Reflection/Named/SyntaxGravatar Jason Gross2017-03-08
* 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
* make 8.5 happyGravatar Andres Erbsen2017-03-02
* remove dangling file that gives a warningGravatar Andres Erbsen2017-03-02
* deleted src/Specific/GF25519ExtendedAddCoordinates.vGravatar Andres Erbsen2017-03-02
* fix src/Specific/GF25519Reflective/Reified/AddCoordinates.vGravatar Andres Erbsen2017-03-02
* use [positive] for [F] modulus, char_ge_C instead of char_gt_CGravatar Andres Erbsen2017-03-02
* Switch to fully uncurried form for reflectionGravatar Jason Gross2017-03-01
* Rename Interp lemmasGravatar Jason Gross2017-02-21
* Add some display logsGravatar Jason Gross2017-02-15
* Add some display logsGravatar Jason Gross2017-02-15
* Add rudimentary Java and C notation files, displayGravatar Jason Gross2017-02-15
* Clean up and improve Reflection.RelationsGravatar Jason Gross2017-02-07
* Split up Reflection/Z/Syntax and make it smallerGravatar Jason Gross2017-02-02
* Split off some bits of Reflection.SyntaxGravatar Jason Gross2017-01-26
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
* Split out Reflection.Equality, change Tflat implicit argumentGravatar Jason Gross2017-01-19
* Add reified LadderStep without carriesGravatar Jason Gross2017-01-07
* Revert "Add apply10"Gravatar Jason Gross2017-01-07
* Add Common10_4OpGravatar Jason Gross2017-01-07
* Add Expr10_4OpGravatar Jason Gross2017-01-07
* Add i10top_correct_and_boundedGravatar Jason Gross2017-01-07
* Add appify10Gravatar Jason Gross2017-01-07
* Admit Common9_4Op.vGravatar Jason Gross2016-12-08
* Fix looping in Coq 8.4 in ExtendedAddCoordinates.vGravatar Jason Gross2016-12-02
* Minor change to inm_op_correct_and_bounded_prefixGravatar Jason Gross2016-11-25
* Fix a typoGravatar Jason Gross2016-11-25
* Add inm_op_correct_and_bounded_iff_prefixGravatar Jason Gross2016-11-25
* Add inm_op_correct_and_boundedGravatar Jason Gross2016-11-25
* uncurry_n_op_fe25519Gravatar Jason Gross2016-11-25
* Various application lemmasGravatar Jason Gross2016-11-23
* More GF25519ReflectiveCommon generalizationGravatar Jason Gross2016-11-22
* Copy bounds, fix a typoGravatar Jason Gross2016-11-22
* Start work on a faster version of GF*Reflective/Common*Gravatar Jason Gross2016-11-21
* Fix missing import for List.repeat in 8.4Gravatar Jason Gross2016-11-21
* Better extractionGravatar Jason Gross2016-11-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-10 14:16:34 +0000