aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-tac.tex
AgeCommit message (Expand)Author
2017-12-14Add doc for Set Debug RAKAM.Gaëtan Gilbert
2017-12-14Add doc for Set Debug Cbv.Gaëtan Gilbert
2017-12-14Add doc for Set Info/Debug Auto/Trivial/Eauto.Gaëtan Gilbert
2017-12-14Add doc for Set Congruence VerboseGaëtan Gilbert
2017-10-24Fix #4846Johannes Kloos
2017-10-24Fix #5413: [unfold ... in] not documentedJohannes Kloos
2017-09-22Avoid generated names for html pages of the reference manual (bug #4742).Guillaume Melquiond
2017-09-01add option index entry for NativeCompute ProfilingPaul Steckler
2017-08-18use OCaml temp_file, instead of our own versionPaul Steckler
2017-08-17Add native compute profiling, BZ#5170Paul Steckler
2017-08-16mention that tactic is the identity or gives errorPaul Steckler
2017-08-16change section caption, improve some wordingPaul Steckler
2017-07-28Fix documentation of Hint Mode (bug #4911).Guillaume Melquiond
2017-07-11Sync the manual with the deprecation warnings.Théo Zimmermann
2017-07-05Merge PR #837: Add inversion_sigma to CHANGES and to docMaxime Dénès
2017-07-04Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-30Add doc for inversion_sigma to RefMan-tacJason Gross
2017-06-19Merge PR#777: Improving documentation of tactic "move" (report #4561)Maxime Dénès
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
2017-06-13Improving documentation of tactic "move" (report #4561).Hugo Herbelin
2017-06-13Document instantiate (ident := term) and make it the preferred variant.Théo Zimmermann
2017-06-01Merge PR#449: make specialize smarter (bug 5370).Maxime Dénès
2017-05-31Documenting the new behaviour of specialize.Pierre Courtieu
2017-05-30Documentation for eassert, eenough, epose proof, eset, eremember, epose.Hugo Herbelin
2017-05-17Documenting relaxing of constraints on injection.Hugo Herbelin
2017-05-04Improve documentation of assert / pose proof / specialize.Théo Zimmermann
2017-04-09Fixing #5420 as well as many related bugs due to miscounting let-ins.Hugo Herbelin
2016-12-06Fix broken documentation in presence of \zeroone{... \tt ...}.Guillaume Melquiond
2016-12-06Update documentation (bugs #5246 and #5251).Guillaume Melquiond
2016-11-08Merge remote-tracking branch 'github/pr/348' into v8.6Maxime Dénès
2016-11-07Merge remote-tracking branch 'github/pr/339' into v8.6Maxime Dénès
2016-11-07Document two new variants of refineMatthieu Sozeau
2016-11-05Minor fix in documentationMatthieu Sozeau
2016-11-04Merge remote-tracking branch 'github/pr/336' into v8.6Maxime Dénès
2016-11-03Lets Hints/Instances take an optional patternMatthieu Sozeau
2016-10-29Documenting changes in typeclassesMatthieu Sozeau
2016-10-25Remove v62 from the refman.Théo Zimmermann
2016-10-24Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-19Documenting Hint Resolve -> and <- variants.Théo Zimmermann
2016-10-19Making the doc of auto hints more precise.Théo Zimmermann
2016-10-18Extending the doc with a general summary of auto variants.Théo Zimmermann
2016-10-18Document info_auto.Théo Zimmermann
2016-10-18Improve the documentation of eauto.Théo Zimmermann
2016-10-03fixing bug 4609: document an option governing the generation of equalitiesYves Bertot
2016-09-30Merge branch 'v8.5' into v8.6Maxime Dénès
2016-09-28Merge remote-tracking branch 'github/pr/232' into v8.6Maxime Dénès
2016-09-27Fixing #4887 (confusion between using and with in documentation of firstorder).Hugo Herbelin
2016-09-15Extending "contradiction" so that it recognizes statements such as "~x=x" or ...Hugo Herbelin
2016-09-12Refolding: disable in 8.4 compat file, documentMatthieu Sozeau
2016-08-21Documenting "Set Structural Injection".Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 05:16:59 +0000