aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-tac.tex
Commit message (Expand)AuthorAge
* 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
* | fixing bug 4609: document an option governing the generation of equalitiesGravatar Yves Bertot2016-10-03
* | Merge branch 'v8.5' into v8.6Gravatar Maxime Dénès2016-09-30
|\|
* | Merge remote-tracking branch 'github/pr/232' into v8.6Gravatar Maxime Dénès2016-09-28
|\ \
| | * Fixing #4887 (confusion between using and with in documentation of firstorder).Gravatar Hugo Herbelin2016-09-27
* | | Extending "contradiction" so that it recognizes statements such as "~x=x" or ...Gravatar Hugo Herbelin2016-09-15
* | | Refolding: disable in 8.4 compat file, documentGravatar Matthieu Sozeau2016-09-12
* | | Documenting "Set Structural Injection".Gravatar Hugo Herbelin2016-08-21