aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
...
* Add Z.pow_nonneg to zarithGravatar Jason Gross2017-04-09
* Make replace_with_neg more powerfulGravatar Jason Gross2017-04-09
* Handle more things in Z.peel_leGravatar Jason Gross2017-04-09
* Add Z.peel_leGravatar Jason Gross2017-04-09
* Add Z.log2_up_le_mono to zarithGravatar Jason Gross2017-04-09
* Add Z.max_le_compat Z.min_le_compat to zarithGravatar Jason Gross2017-04-09
* Add lemmas about shift bounds to ZUtilGravatar Jason Gross2017-04-09
* Fix missing unfoldGravatar Jason Gross2017-04-09
* Add sub_le_flip_le_ProperGravatar Jason Gross2017-04-09
* Add Z.shift{l,r}_opp_lGravatar Jason Gross2017-04-08
* Add some le proper flip lemmasGravatar Jason Gross2017-04-08
* Use Z.max 0, not an if statementGravatar Jason Gross2017-04-08
* Add wordToZ_ZToWord_mod_fullGravatar Jason Gross2017-04-08
* Add wordToZ_ZToWord_modGravatar Jason Gross2017-04-08
* Add ZToWord_wordToZ_ZToWord_smallGravatar Jason Gross2017-04-08
* Make dlet-moving on sigma goals use changeGravatar Jason Gross2017-04-07
* Merge branch 'rename-everything'. Closes #14.Gravatar Andres Erbsen2017-04-06
|\
| * rename-everythingGravatar Andres Erbsen2017-04-06
* | Faster clear_all tacticGravatar Jason Gross2017-04-06
| * start removing BaseSystemGravatar Andres Erbsen2017-04-06
| * do not use VerdiTactics in files we plan to keepGravatar Andres Erbsen2017-04-06
|/
* Export ClearAll in TacticsGravatar Jason Gross2017-04-06
* More vigorous clearing in unify_transformed_rhs_abstract_tacGravatar Jason Gross2017-04-06
* Add clear_allGravatar Jason Gross2017-04-06
* make elliptic curve proofs faster and split them into filesGravatar Andres Erbsen2017-04-05
* Don't clutter up typeclass log with cidtacGravatar Jason Gross2017-04-05
* Fix transparent assert by to respect namesGravatar Jason Gross2017-04-05
* Add TransparentAssertGravatar Jason Gross2017-04-05
* Remove bad [Local]Gravatar Jason Gross2017-04-05
* Actually add ChangeInAllGravatar Jason Gross2017-04-05
* Add Tactics.ChangeInAllGravatar Jason Gross2017-04-05
* Fix bug in change_with_curriedGravatar Jason Gross2017-04-05
* When currying, change with curried form in *Gravatar Jason Gross2017-04-05
* Add Tactics.MoveLetInGravatar Jason Gross2017-04-05
* Add Tactics.PrintContextGravatar Jason Gross2017-04-04
* Add [Proof using] to most proofsGravatar Jason Gross2017-04-04
* Move sigma MapProjections to a separate fileGravatar Jason Gross2017-04-04
* Add Tuple.map_ProperGravatar Jason Gross2017-04-03
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
* Split off liftn_sig, add lift{3,4}_sigGravatar Jason Gross2017-04-03
* Fix parsing issueGravatar Jason Gross2017-04-03
* Add proj2_sig_mapGravatar Jason Gross2017-04-03
* Don't require keeping track of which goals have evars; check that in tacticsGravatar Jason Gross2017-04-03
* Add UnifyAbstractReflexivity tacticsGravatar Jason Gross2017-04-03
* Fix a typoGravatar Jason Gross2017-04-02
* Add projT2_mapGravatar Jason Gross2017-04-02
* Add Tactics.EvarExistsGravatar Jason Gross2017-04-02
* Add Util.SigmaAssocGravatar Jason Gross2017-04-02
* Add ap_transport to Equality.vGravatar Jason Gross2017-04-02
* Coalesce Tuple.pointwise2 and Tuple.fieldwiseGravatar Jason Gross2017-04-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 00:25:31 +0000