aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-tac.tex
Commit message (Expand)AuthorAge
* 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
* | | Add and document match, fix and cofix reduction flags.Gravatar Maxime Dénès2016-07-01
| * | Update the documentation for goal selectors.Gravatar Cyprien Mangin2016-06-30
|/ /
* | Updated CHANGES about subst. More on recursive equations in reference manual.Gravatar Hugo Herbelin2016-06-29
* | Document new Hint Mode option.Gravatar Matthieu Sozeau2016-06-16
* | Revise syntax of Hint CutGravatar Matthieu Sozeau2016-06-16
* | Add documentation for goal selectors.Gravatar Cyprien Mangin2016-06-14
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\|
| * In Regular Subst Tactic mode, ensure that the order of hypotheses isGravatar Hugo Herbelin2016-05-03
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\|
| * Document Hint Mode, cleanup Hint doc.Gravatar Matthieu Sozeau2016-02-24
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Clarifying the documentation of tactics "cbv" and "lazy".Gravatar Hugo Herbelin2016-01-20
* | Updating and improving the documentation of intros patterns.Gravatar Hugo Herbelin2016-01-14
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-13
|\|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 04:15:23 +0000