| Commit message (Expand) | Author | Age |
* | Fixing inversion after having fixed intros_replacing | Hugo Herbelin | 2014-09-10 |
* | Removing "eqn:" for "induction" in reference manual. | Hugo Herbelin | 2014-09-10 |
* | Doc: [revgoals]. | Arnaud Spiwack | 2014-09-08 |
* | Little fix in documentation of inversion. | Hugo Herbelin | 2014-09-07 |
* | Cbn in refman | Pierre Boutillier | 2014-09-03 |
* | "allows to", like "allowing to", is improper | Jason Gross | 2014-08-25 |
* | 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-18 |
* | 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-08-05 |
* | Typos. | Hugo Herbelin | 2014-07-31 |
* | 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-07-25 |
* | More on injection over a projectable "existT". - Fixing syntax "injection ...... | Hugo Herbelin | 2014-05-31 |
* | Fix for bug #3107. | Guillaume Melquiond | 2014-04-04 |
* | fixing Function doc | Julien Forest | 2014-04-04 |
* | Fix Bug 3131 + Really drop mentions of info in refman. | Pierre Boutillier | 2014-04-02 |
* | Documenting the tactic-in-term construction. | Pierre-Marie Pédrot | 2013-12-11 |
* | Silence some warning about references in documentation. | Guillaume Melquiond | 2013-12-03 |
* | 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-11-02 |
* | add "Print Ring" and "Print Field" vernacular commands | gareuselesinge | 2013-08-30 |
* | Manual fixed w.r.t. STM | gareuselesinge | 2013-08-08 |
* | Documenting the Remove Hints command. | ppedrot | 2013-08-01 |
* | Revising r16550 about providing intro patterns for applying injection: | herbelin | 2013-07-09 |
* | Making the behavior of "injection ... as ..." more natural: | herbelin | 2013-06-02 |
* | Fixing a typo in the documentation of discriminate. | herbelin | 2013-06-02 |
* | Documenting the previous commit. | ppedrot | 2013-05-12 |
* | Fix typo in manual | gareuselesinge | 2013-05-06 |
* | 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 | 2013-03-21 |
* | RefMan-tac: fix a few glitches concerning the documentation of eqn: | letouzey | 2012-10-23 |
* | 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-16 |
* | Port rewrites of tactic documentation from branch 8.4. | gmelquio | 2012-09-15 |
* | Improving rendering of ldots in doc (partially done, there are too | herbelin | 2012-08-11 |
* | 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-09 |
* | Open Local Scope ---> Local Open Scope, same with Notation and alii | letouzey | 2012-07-05 |
* | Uniformisation in the documentation: remove the use of 'coinductive' in | aspiwack | 2012-04-13 |
* | Document the [unify] tactic. | msozeau | 2012-02-18 |
* | Added the btauto tactic to the documentation. | ppedrot | 2012-01-19 |
* | Reference Manual: misc fixes (spelling, index, updating pre-8.0 syntax). | herbelin | 2011-12-26 |