aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tactics.v
Commit message (Expand)AuthorAge
* More fine-grained util tactic filesGravatar Jason Gross2017-01-17
* Add convoy_destructGravatar Jason Gross2016-11-07
* Add break_innermost_matchGravatar Jason Gross2016-10-30
* Add tactics to implement better fraction removalGravatar Jason Gross2016-10-26
* specialize_by: only specialize arguments of type [Prop]Gravatar Andres Erbsen2016-10-10
* specialize_by: explicitly maintain transparencyGravatar Andres Erbsen2016-10-10
* Don't zeta-reduce in [simplify_projections]Gravatar Jason Gross2016-09-02
* Strip <infomsg>; it messes things up in Coq 8.6 displayGravatar Jason Gross2016-09-02
* Slightly better cfailGravatar Jason Gross2016-09-02
* Add cfail{2,3}Gravatar Jason Gross2016-09-02
* Add [idtac_goal]Gravatar Jason Gross2016-09-02
* Add constr-based idtac tacticsGravatar Jason Gross2016-09-02
* Moved a tactic to Util/Tactics.vGravatar jadep2016-08-24
* Add simplify_projections to Util.TacticsGravatar Jason Gross2016-08-17
* Add [Z.linear_solve_for], [Z.linear_substitute]Gravatar Jason Gross2016-08-17
* Don't take advantage of design flaws (auto with *)Gravatar Jason Gross2016-08-11
* Add [especialize], [forward], [eforward]Gravatar Jason Gross2016-08-10
* Add tactics to simplify repeated conditionsGravatar Jason Gross2016-08-09
* Add erewrite_hyp tacticsGravatar Jason Gross2016-08-08
* 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-15 20:52:57 +0000