aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-tac.tex
AgeCommit message (Expand)Author
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
2016-01-12Documenting dtauto and dintuition.Hugo Herbelin
2016-01-12Documenting options "Intuition Negation Unfolding", "Intuition Iff Unfolding".Hugo Herbelin
2016-01-12Documenting option 'Set Bracketing Last Introduction Pattern'.Hugo Herbelin
2016-01-12restore documentation of admitEnrico Tassi
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-16Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Guillaume Melquiond
2015-12-15Simplifying documentation of "assert form as pat".Hugo Herbelin
2015-12-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-10Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Hugo Herbelin
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-07Fix some typos.Guillaume Melquiond
2015-12-05Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Hugo Herbelin
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 08:03:07 +0000