aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-tac.tex
AgeCommit message (Expand)Author
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
2016-07-01Add and document match, fix and cofix reduction flags.Maxime Dénès
2016-06-30Update the documentation for goal selectors.Cyprien Mangin
2016-06-29Updated CHANGES about subst. More on recursive equations in reference manual.Hugo Herbelin
2016-06-16Document new Hint Mode option.Matthieu Sozeau
2016-06-16Revise syntax of Hint CutMatthieu Sozeau
2016-06-14Add documentation for goal selectors.Cyprien Mangin
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-03In Regular Subst Tactic mode, ensure that the order of hypotheses isHugo Herbelin
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-24Document Hint Mode, cleanup Hint doc.Matthieu Sozeau
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Clarifying the documentation of tactics "cbv" and "lazy".Hugo Herbelin
2016-01-14Updating and improving the documentation of intros patterns.Hugo Herbelin
2016-01-13Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 00:53:14 +0000