aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-tac.tex
Commit message (Expand)AuthorAge
* [Sphinx] Move chapter 8 to new infrastructureGravatar Maxime Dénès2018-03-15
* [compat] Remove "Refolding Reduction" option.Gravatar Emilio Jesus Gallego Arias2018-03-08
* Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"Gravatar Maxime Dénès2018-03-06
|\
* \ Merge PR #915: Fix rewrite in * side conditionsGravatar Maxime Dénès2018-03-04
|\ \
| | * [compat] Remove "Intuition Iff Unfolding"Gravatar Emilio Jesus Gallego Arias2018-03-03
| |/ |/|
| * Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Gravatar Hugo Herbelin2018-03-01
* | Typo in the documentation of the `pattern` tacticGravatar Joachim Breitner2018-02-27
|/
* Add doc for Set Debug RAKAM.Gravatar Gaëtan Gilbert2017-12-14
* Add doc for Set Debug Cbv.Gravatar Gaëtan Gilbert2017-12-14
* Add doc for Set Info/Debug Auto/Trivial/Eauto.Gravatar Gaëtan Gilbert2017-12-14
* Add doc for Set Congruence VerboseGravatar Gaëtan Gilbert2017-12-14
* Fix #4846Gravatar Johannes Kloos2017-10-24
* Fix #5413: [unfold ... in] not documentedGravatar Johannes Kloos2017-10-24
* Avoid generated names for html pages of the reference manual (bug #4742).Gravatar Guillaume Melquiond2017-09-22
* add option index entry for NativeCompute ProfilingGravatar Paul Steckler2017-09-01
* use OCaml temp_file, instead of our own versionGravatar Paul Steckler2017-08-18
* Add native compute profiling, BZ#5170Gravatar Paul Steckler2017-08-17
* mention that tactic is the identity or gives errorGravatar Paul Steckler2017-08-16
* change section caption, improve some wordingGravatar Paul Steckler2017-08-16
* Fix documentation of Hint Mode (bug #4911).Gravatar Guillaume Melquiond2017-07-28
* Sync the manual with the deprecation warnings.Gravatar Théo Zimmermann2017-07-11
* Merge PR #837: Add inversion_sigma to CHANGES and to docGravatar Maxime Dénès2017-07-05
|\
* \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\ \
| | * Add doc for inversion_sigma to RefMan-tacGravatar Jason Gross2017-06-30
| |/ |/|
* | Merge PR#777: Improving documentation of tactic "move" (report #4561)Gravatar Maxime Dénès2017-06-19
|\ \
* | | Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
| * | Improving documentation of tactic "move" (report #4561).Gravatar Hugo Herbelin2017-06-13
|/ /
| * Document instantiate (ident := term) and make it the preferred variant.Gravatar Théo Zimmermann2017-06-13
* | Merge PR#449: make specialize smarter (bug 5370).Gravatar Maxime Dénès2017-06-01
|\ \
| * | Documenting the new behaviour of specialize.Gravatar Pierre Courtieu2017-05-31
* | | Documentation for eassert, eenough, epose proof, eset, eremember, epose.Gravatar Hugo Herbelin2017-05-30
|/ /
* | Documenting relaxing of constraints on injection.Gravatar Hugo Herbelin2017-05-17
* | Improve documentation of assert / pose proof / specialize.Gravatar Théo Zimmermann2017-05-04
* | Fixing #5420 as well as many related bugs due to miscounting let-ins.Gravatar Hugo Herbelin2017-04-09
|/
* Fix broken documentation in presence of \zeroone{... \tt ...}.Gravatar Guillaume Melquiond2016-12-06
* Update documentation (bugs #5246 and #5251).Gravatar Guillaume Melquiond2016-12-06
* Merge remote-tracking branch 'github/pr/348' into v8.6Gravatar Maxime Dénès2016-11-08
|\
* \ Merge remote-tracking branch 'github/pr/339' into v8.6Gravatar Maxime Dénès2016-11-07
|\ \
| * | Document two new variants of refineGravatar Matthieu Sozeau2016-11-07
| | * Minor fix in documentationGravatar Matthieu Sozeau2016-11-05
| |/ |/|
* | Merge remote-tracking branch 'github/pr/336' into v8.6Gravatar Maxime Dénès2016-11-04
|\ \
| | * Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
| | * Documenting changes in typeclassesGravatar Matthieu Sozeau2016-10-29
| |/ |/|
| * Remove v62 from the refman.Gravatar Théo Zimmermann2016-10-25
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-24
|\ \ | |/ |/|
| * Documenting Hint Resolve -> and <- variants.Gravatar Théo Zimmermann2016-10-19
| * Making the doc of auto hints more precise.Gravatar Théo Zimmermann2016-10-19
| * Extending the doc with a general summary of auto variants.Gravatar Théo Zimmermann2016-10-18
| * Document info_auto.Gravatar Théo Zimmermann2016-10-18
| * Improve the documentation of eauto.Gravatar Théo Zimmermann2016-10-18