aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/Z
Commit message (Expand)AuthorAge
* Add cast_back_flat_constGravatar Jason Gross2017-03-22
* Make Z.ltb_to_lt a bit strongerGravatar Jason Gross2017-03-21
* Add dummy TWord constructor to syntax typeGravatar Jason Gross2017-03-19
* make 8.5 happyGravatar Andres Erbsen2017-03-02
* Switch to fully uncurried form for reflectionGravatar Jason Gross2017-03-01
* Add BoundsInterpretationsGravatar Jason Gross2017-02-23
* Add various reflection improvements, boundbycastGravatar Jason Gross2017-02-21
* Rename Interp lemmasGravatar Jason Gross2017-02-21
* Add rudimentary Java and C notation files, displayGravatar Jason Gross2017-02-15
* Add files for constant reflective notationsGravatar Jason Gross2017-02-10
* Clean up and improve Reflection.RelationsGravatar Jason Gross2017-02-07
* Move things from WordUtil to ZUtil, add word lemmaGravatar Jason Gross2017-02-06
* Reorder Reflection.Z.SyntaxGravatar Jason Gross2017-02-02
* Split up Reflection/Z/Syntax and make it smallerGravatar Jason Gross2017-02-02
* Add invert_match_opGravatar Jason Gross2017-02-01
* Add invert_opGravatar Jason Gross2017-02-01
* 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
* Various application lemmasGravatar Jason Gross2016-11-23
* Remove an admitGravatar Jason Gross2016-11-17
* 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
| * More factoring in related_Z_opGravatar Jason Gross2016-11-08
| * Fix some qualified name issues with previous commitGravatar Jason Gross2016-11-08
| * Add word64ToZ_{neg,cmovne,cmovle,conditional_subtract}Gravatar Jason Gross2016-11-08
| * Remove lor admit in relationsGravatar Jason Gross2016-11-08
| * Minor refactoring of related_Z_opGravatar Jason Gross2016-11-07
| * Finish related_bounds_t_map1_tuple2Gravatar Jason Gross2016-11-07
| * More progress on related_bounds_t_map1_tuple2Gravatar Jason Gross2016-11-07
| * More progress on t_map1_tuple2 lemmasGravatar Jason Gross2016-11-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 21:22:20 +0000