aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
...
* Add appify10Gravatar Jason Gross2017-01-07
* Add more generic ladderstepGravatar Jason Gross2017-01-07
* Better word operationsGravatar Jason Gross2017-01-03
* Add word versions of ModularBaseSystemListZOperationsGravatar Jason Gross2017-01-03
* Add ZToWord,wordToZGravatar Jason Gross2017-01-03
* Add fixed word size definitionsGravatar Jason Gross2017-01-03
* Fixes for Coq 8.4Gravatar Jason Gross2017-01-03
* Add src/Reflection/MapCastWithCastOp.vGravatar Jason Gross2017-01-01
* Remove [Print]Gravatar Jason Gross2017-01-01
* Redo MultiSizeTest with generic frameworkGravatar Jason Gross2017-01-01
* Transparent versions of {flat_,}type_eq_decGravatar Jason Gross2017-01-01
* Add generic code for MultiSizeTestGravatar Jason Gross2017-01-01
* Add smart_interp_map_genGravatar Jason Gross2017-01-01
* Add SmartFlatTypeMap2Gravatar Jason Gross2016-12-26
* Add flatten_flat_typeGravatar Jason Gross2016-12-26
* Fix Coq 8.6 warningsGravatar Jason Gross2016-12-26
* MultiSizeTest: a basic example of the scheme I have in mind for bounds infere...Gravatar Adam Chlipala2016-12-25
* Fix 8.4 build issuesGravatar Jason Gross2016-12-15
* Fix 8.4 issuesGravatar Jason Gross2016-12-15
* Work around bug in 8.4 implicitsGravatar Jason Gross2016-12-14
* Work around bug in 8.4 applyGravatar Jason Gross2016-12-14
* Admit Common9_4Op.vGravatar Jason Gross2016-12-08
* Don't use UIP in inversion_wffGravatar Jason Gross2016-12-03
* Add inversion_wffGravatar Jason Gross2016-12-03
* Add WfInversionGravatar Jason Gross2016-12-03
* More powerful inversion_optionGravatar Jason Gross2016-12-03
* Move things to ExprInversionGravatar Jason Gross2016-12-03
* Add invert_VarGravatar Jason Gross2016-12-03
* Arguments for invert_OpGravatar Jason Gross2016-12-03
* Fewer autogenerated namesGravatar Jason Gross2016-12-03
* Add invert_OpGravatar Jason Gross2016-12-03
* Change some default namesGravatar Jason Gross2016-12-03
* copy_bounds.shGravatar Jason Gross2016-12-02
* Fix looping in Coq 8.4 in ExtendedAddCoordinates.vGravatar Jason Gross2016-12-02
* Initial (not fully working) version of MapWithInterpInfoGravatar Jason Gross2016-12-02
* Add SmartFlatTypeMapUnInterpGravatar Jason Gross2016-12-02
* Add invert_LetInGravatar Jason Gross2016-12-02
* Arguments for invert_PairGravatar Jason Gross2016-12-02
* Add invert_PairGravatar Jason Gross2016-12-02
* Add SmartFlatTypeMapInterpGravatar Jason Gross2016-12-02
* SmartFlatTypeMap argumentsGravatar Jason Gross2016-12-02
* Add SmartFlatTypeMapGravatar 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
* Also git add in copy_boundsGravatar 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 13:30:40 +0000