aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection
Commit message (Expand)AuthorAge
* Preserve names in invert_expr_substGravatar Jason Gross2017-01-23
* Make invert_expr_subst not loopGravatar Jason Gross2017-01-23
* Fix invert_expr_substGravatar Jason Gross2017-01-23
* Better invert_exprGravatar Jason Gross2017-01-23
* Minor additionsGravatar Jason Gross2017-01-23
* Fix a typoGravatar Jason Gross2017-01-23
* Add invert_expr_substGravatar Jason Gross2017-01-23
* Allow inversion on wff if either side is not a varGravatar Jason Gross2017-01-23
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
* Make f_equal2 transparent in equality proofGravatar Jason Gross2017-01-19
* Split out Reflection.Equality, change Tflat implicit argumentGravatar Jason Gross2017-01-19
* More fine-grained util tactic filesGravatar Jason Gross2017-01-17
* Add ApplicationRelationsGravatar Jason Gross2017-01-10
* Add Syntax.tuple_mapGravatar Jason Gross2017-01-09
* 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
* 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
* 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
* Various application lemmasGravatar Jason Gross2016-11-23
* Add lemmas about applicationGravatar Jason Gross2016-11-22
* Add interp_all_binders_for'Gravatar Jason Gross2016-11-22
* Remove an admitGravatar Jason Gross2016-11-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 19:16:09 +0000