aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Add ApplicationRelationsGravatar Jason Gross2017-01-10
* Add Syntax.tuple_mapGravatar Jason Gross2017-01-09
* Add >>> reserved notationGravatar Jason Gross2017-01-09
* Add Zmod_to_equiv_moduloGravatar Jason Gross2017-01-09
* copy_boundsGravatar Jason Gross2017-01-07
* Add reified LadderStep without carriesGravatar Jason Gross2017-01-07
* Add ladderstep_other_assocGravatar Jason Gross2017-01-07
* Revert "Add apply10"Gravatar Jason Gross2017-01-07
* Add apply10Gravatar Jason Gross2017-01-07
* copy_boundsGravatar 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
* 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