aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tactics.v
Commit message (Expand)AuthorAge
* Add constr_fail and constr_fail_withGravatar Jason Gross2019-03-31
* Remove GlobalTacticalsGravatar Jason Gross2019-03-08
* Add some gtacticsGravatar Jason Gross2019-03-08
* Add has_body tacticGravatar Jason Gross2018-12-21
* Add CPSId tacticsGravatar Jason Gross2018-10-28
* Export more tactics in Tactics.vGravatar Jason Gross2018-10-10
* Add specialize_all_ways, fix a proof in src/Compilers/Z/ArithmeticSimplifierI...Gravatar Jason Gross2018-06-26
* Add CacheTermGravatar Jason Gross2017-10-17
* Add PoseTermWithNameGravatar Jason Gross2017-10-05
* Add UnfoldArgGravatar Jason Gross2017-07-08
* Add script to remake Tactics.v fileGravatar Jason Gross2017-06-11
* Export ClearAll in TacticsGravatar Jason Gross2017-04-06
* Add TransparentAssertGravatar Jason Gross2017-04-05
* Add Tactics.ChangeInAllGravatar Jason Gross2017-04-05
* Add Tactics.MoveLetInGravatar Jason Gross2017-04-05
* Add Tactics.PrintContextGravatar Jason Gross2017-04-04
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
* Add UnifyAbstractReflexivity tacticsGravatar Jason Gross2017-04-03
* Add Tactics.EvarExistsGravatar Jason Gross2017-04-02
* Split out Tactics.SubstLetGravatar Jason Gross2017-04-01
* Add [etransitivity y], [etransitivity_rev] tacticsGravatar Jason Gross2017-03-31
* address some code review commentsGravatar Andres Erbsen2017-03-02
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
* speed up NewBaseystem synthesisGravatar Andres Erbsen2017-02-23
* Split off unique {pose,assert}Gravatar Jason Gross2017-01-31
* Split off some bits of Reflection.SyntaxGravatar Jason Gross2017-01-26
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-29 20:50:05 +0000