aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tactics.v
Commit message (Expand)AuthorAge
* Add reverse_nondep and ring_simplify_subterms_in_all tacticsGravatar Jason Gross2016-07-22
* Make the library 20% faster: [auto with *] is evilGravatar Jason Gross2016-07-22
* Add ring_simplify_subtermsGravatar Jason Gross2016-07-22
* Merge of fixedlength and masterGravatar jadep2016-07-11
|\
| * wrap nsatz in AlgebraGravatar Andres Erbsen2016-07-11
| * Add useful tactics and util lemmasGravatar Jason Gross2016-07-08
* | stuck trying to figure out dependently typed continuation passing styleGravatar Andres Erbsen2016-07-06
|/
* Add [specialize_by] tacticGravatar Jason Gross2016-07-01
* Fix field_algebra in 8.4Gravatar Jason Gross2016-06-28
* Fix super_nsatz tactic to be better about orderingGravatar Jason Gross2016-06-28
* Add [destruct_head] tacticsGravatar Jason Gross2016-06-27
* Add [break_match] for hypothesesGravatar Jason Gross2016-06-27
* Various nsatz and field tactic improvementsGravatar Jason Gross2016-06-24
* Improve some tactics and lemmasGravatar Jason Gross2016-06-23
* [break_match] should not be localGravatar Jason Gross2016-06-23
* Add tactics to Tactics, at most 2 sq-roots to AlgebraGravatar Jason Gross2016-06-23
* Add a tactic for field inequalitiesGravatar Jason Gross2016-04-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-04 19:31:18 +0000