aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection
Commit message (Expand)AuthorAge
* 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
* Add interpf_LetInGravatar Jason Gross2016-11-17
* : assert is not valid 8.4 syntaxGravatar Jason Gross2016-11-17
* Add Un{Return,Abs}_etaGravatar Jason Gross2016-11-16
* Add : assert to a bunch of argumentsGravatar Jason Gross2016-11-16
* Split fixedpoint in interpfGravatar Jason Gross2016-11-16
* Arguments for Un{Return,Abs}Gravatar Jason Gross2016-11-16
* Add UnReturn, UnAbsGravatar Jason Gross2016-11-16
* Support for 128-bit wordsGravatar Jason Gross2016-11-14
* Add word-size-independent interpretationsGravatar Jason Gross2016-11-14
* Fix reification of negGravatar Jason Gross2016-11-11
* Make [neg] a unary operation in reflectionGravatar Jason Gross2016-11-11
* Remove more conditional subtractGravatar Jason Gross2016-11-11
* Remove extra conditional subtract thingsGravatar Jason Gross2016-11-11
* Remove special code for reified conditional subGravatar Jason Gross2016-11-11
* More proof fixesGravatar Jason Gross2016-11-10
* Minimize diff with master, fix some proofs that were brokenGravatar Jason Gross2016-11-10
* Merge with masterGravatar Rob Sloan2016-11-09
|\
| * Fix for 8.4Gravatar Jason Gross2016-11-09
| * Switch to accurate bounds for lorGravatar Jason Gross2016-11-09
* | Rebase + remove WordizeUtil dependency from Z/InterpretationsGravatar Rob Sloan2016-11-09
|\ \
| | * Remove last admitted lemma in src/Reflection/Z/Interpretations/Relations.vGravatar Jason Gross2016-11-09
| |/
* | Finished WordUtil, word operations in Z/InterpretationGravatar Rob Sloan2016-11-09
* | Not quite done with WordUtil lemmas.Gravatar Robert Sloan2016-11-08
|\ \
| | * Fix for Coq 8.4Gravatar Jason Gross2016-11-08
| | * Some fixes for 8.4 differencesGravatar Jason Gross2016-11-08
| | * More progress on src/Reflection/Z/Interpretations/Relations.vGravatar Jason Gross2016-11-08
| | * Fix 8.4 build ([value] is a constant)Gravatar Jason Gross2016-11-08
| |/
| * Factor related_Z_op (except conditional_sub)Gravatar Jason Gross2016-11-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-22 16:47:40 +0000