| Age | Commit message (Expand) | Author |
|---|
| 2014-09-10 | Fixing inversion after having fixed intros_replacing | Hugo Herbelin |
| 2014-09-10 | Removing "eqn:" for "induction" in reference manual. | Hugo Herbelin |
| 2014-09-08 | Doc: [revgoals]. | Arnaud Spiwack |
| 2014-09-07 | Little fix in documentation of inversion. | Hugo Herbelin |
| 2014-09-03 | Cbn in refman | Pierre Boutillier |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 2014-08-18 | Adding a new intro-pattern for "apply in" on the fly. Using syntax | Hugo Herbelin |
| 2014-08-18 | Slight simplification of naming of tactics in equality.ml (hopefully). | Hugo Herbelin |
| 2014-08-05 | Experimentally adding an option for automatically erasing an | Hugo Herbelin |
| 2014-08-05 | Adding a syntax "enough" for the variant of "assert" with the order of | Hugo Herbelin |
| 2014-07-31 | Typos. | Hugo Herbelin |
| 2014-07-25 | Document swap tactic. | Arnaud Spiwack |
| 2014-07-25 | Document cycle tactic. | Arnaud Spiwack |
| 2014-07-25 | Warns about inconsistency of generated name in evars and goals. | Arnaud Spiwack |
| 2014-05-31 | More on injection over a projectable "existT". - Fixing syntax "injection ...... | Hugo Herbelin |
| 2014-04-04 | Fix for bug #3107. | Guillaume Melquiond |
| 2014-04-04 | fixing Function doc | Julien Forest |
| 2014-04-02 | Fix Bug 3131 + Really drop mentions of info in refman. | Pierre Boutillier |
| 2013-12-11 | Documenting the tactic-in-term construction. | Pierre-Marie Pédrot |
| 2013-12-03 | Silence some warning about references in documentation. | Guillaume Melquiond |
| 2013-11-02 | Doc: solve the bad interaction between Declare Implicit Tactic and refine. | aspiwack |
| 2013-11-02 | Adds a tactic give_up. | aspiwack |
| 2013-11-02 | A tactic shelve_unifiable. | aspiwack |
| 2013-11-02 | Adds a shelve tactic. | aspiwack |
| 2013-11-02 | Document "all:" and "Set Default Goal Selector". | aspiwack |
| 2013-08-30 | add "Print Ring" and "Print Field" vernacular commands | gareuselesinge |
| 2013-08-08 | Manual fixed w.r.t. STM | gareuselesinge |
| 2013-08-01 | Documenting the Remove Hints command. | ppedrot |
| 2013-07-09 | Revising r16550 about providing intro patterns for applying injection: | herbelin |
| 2013-06-02 | Making the behavior of "injection ... as ..." more natural: | herbelin |
| 2013-06-02 | Fixing a typo in the documentation of discriminate. | herbelin |
| 2013-05-12 | Documenting the previous commit. | ppedrot |
| 2013-05-06 | Fix typo in manual | gareuselesinge |
| 2013-03-21 | Using hnf instead of "intro H" for forcing reduction to a product. | herbelin |
| 2013-03-21 | Fixing an old pecularity of "red": head betaiota redexes are now | herbelin |
| 2012-10-23 | RefMan-tac: fix a few glitches concerning the documentation of eqn: | letouzey |
| 2012-09-16 | Move reflexivity, symmetry, and transitivity, next to f_equal, in the documen... | gmelquio |
| 2012-09-16 | Some more fixes to tactic documentation. | gmelquio |
| 2012-09-16 | Beautify tactic documentation a bit more. | gmelquio |
| 2012-09-16 | Remove superfluous spaces and commas in tactic documentation. | gmelquio |
| 2012-09-16 | Fix index generation for the pdf document. | gmelquio |
| 2012-09-15 | Port rewrites of tactic documentation from branch 8.4. | gmelquio |
| 2012-08-11 | Improving rendering of ldots in doc (partially done, there are too | herbelin |
| 2012-07-09 | The tactic remember now accepts a final eqn:H option (grant wish #2489) | letouzey |
| 2012-07-09 | induction/destruct : nicer syntax for generating equations (solves #2741) | letouzey |
| 2012-07-05 | Open Local Scope ---> Local Open Scope, same with Notation and alii | letouzey |
| 2012-04-13 | Uniformisation in the documentation: remove the use of 'coinductive' in | aspiwack |
| 2012-02-18 | Document the [unify] tactic. | msozeau |
| 2012-01-19 | Added the btauto tactic to the documentation. | ppedrot |
| 2011-12-26 | Reference Manual: misc fixes (spelling, index, updating pre-8.0 syntax). | herbelin |
