aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
* Better type_inversionGravatar Jason Gross2017-02-13
* Split off inversion_wff for constr-only hypsGravatar Jason Gross2017-02-13
* Add inversion_typeGravatar Jason Gross2017-02-13
* Generalize InlineWfGravatar Jason Gross2017-02-13
* Add SmartCast{Interp,Wf}Gravatar Jason Gross2017-02-13
* Split up BoundByCastGravatar Jason Gross2017-02-13
* Generalize BoundByCast a bitGravatar Jason Gross2017-02-10
* Add EtaInterp, EtaWfGravatar Jason Gross2017-02-10
* Use Eta in BoundByCastGravatar Jason Gross2017-02-10
* Add Reflection/Eta.vGravatar Jason Gross2017-02-10
* Fix a missing section close in ZToRingGravatar Jason Gross2017-02-10
* Add files for constant reflective notationsGravatar Jason Gross2017-02-10
* Accidentally pushed wrong file in last commit; this is the correct oneGravatar jadep2017-02-10
* added ZToRing to _CoqProjectGravatar jadep2017-02-09
* Added ZToRing lemmasGravatar jadep2017-02-09
* Remove useless importsGravatar Jason Gross2017-02-08
* Factor things into BoundByCast.vGravatar Jason Gross2017-02-08
* Fix type inference bug in 8.6Gravatar Jason Gross2017-02-08
* Simpler version of MapCastGravatar Jason Gross2017-02-08
* Remove the let-in from SmartValfGravatar Jason Gross2017-02-07
* Fix relation relb argumentsGravatar Jason Gross2017-02-07
* Add things like interp_flat_type_rel_pointwise1_gen_Prop_iff_boolGravatar Jason Gross2017-02-07
* Clean up and improve Reflection.RelationsGravatar Jason Gross2017-02-07
* Add ZUtil lemmasGravatar Jason Gross2017-02-06
* Add interp_flat_type_rel_pointwise2_flatten_binding_listGravatar Jason Gross2017-02-06
* Move things from WordUtil to ZUtil, add word lemmaGravatar Jason Gross2017-02-06
* field_nsatzGravatar Andres Erbsen2017-02-06
* Fix changed namesGravatar Jason Gross2017-02-03
* Split off non-unfolding version of fixed_size_op_to_wordGravatar Jason Gross2017-02-03
* Add valid_update lemmas about FixedWordSizesGravatar Jason Gross2017-02-03
* Don't unfold wordToZ_gen in fixed_Size_op_to_wordGravatar Jason Gross2017-02-03
* More zutilGravatar Jason Gross2017-02-03
* Add lemmas about bounds of Z.lor, and add Z.max_log2_upGravatar Jason Gross2017-02-03
* Fix a missing argumentGravatar Jason Gross2017-02-03
* Fix a typoGravatar Jason Gross2017-02-03
* Handle more kinds of ops in fixed_size_op_to_wordGravatar Jason Gross2017-02-03
* Only unfold the non-zpecialized versions of wcmovl, wcmovne, wnegGravatar Jason Gross2017-02-03
* Also unfold wcmovl, wcmovne, wneg in fixed_size_constantsGravatar Jason Gross2017-02-03
* Don't autounfold wordToZ nor ZToWordGravatar Jason Gross2017-02-03
* Add fixed_size_op_to_word tacticGravatar Jason Gross2017-02-03
* Add interp_flat_type_rel_pointwise2_hetero_iffGravatar Jason Gross2017-02-03
* Add lemmas for Z ops ProperGravatar Jason Gross2017-02-03
* Add log2_up_le_fullGravatar Jason Gross2017-02-03
* Add Z.log2_up_nonneg to zarithGravatar Jason Gross2017-02-03
* Reorder Reflection.Z.SyntaxGravatar Jason Gross2017-02-02
* Split up Reflection/Z/Syntax and make it smallerGravatar Jason Gross2017-02-02
* Add wf databaseGravatar Jason Gross2017-02-01
* Generalize InlineInterpGravatar Jason Gross2017-02-01
* Fix lazymatch orderingGravatar Jason Gross2017-02-01
* More powerful preinvert_one_typeGravatar Jason Gross2017-02-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 11:29:56 +0000