aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\
| * 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
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\| |
| * | fixing bug 4609: document an option governing the generation of equalitiesGravatar Yves Bertot2016-10-03
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\| |
| * | Merge remote-tracking branch 'github/pr/280' into v8.6Gravatar Maxime Dénès2016-09-30
| |\ \
| * \ \ 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
* | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\| | | |
| * | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-23
| |\ \ \ \ | | | |/ / | | |/| |
| | * | | Replace { command ; } with ( command )Gravatar Erik Martin-Dorel2016-09-19
| | * | | Fix typos in RefMan-uti.tex.Gravatar Erik Martin-Dorel2016-09-19
| | | | * Doc: [Reset Ltac Profile] is not synchronizedGravatar Jason Gross2016-09-16
| | |_|/ | |/| |
| * | | Extending "contradiction" so that it recognizes statements such as "~x=x" or ...Gravatar Hugo Herbelin2016-09-15
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-14
|\| | |
| * | | Refolding: disable in 8.4 compat file, documentGravatar Matthieu Sozeau2016-09-12
* | | | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \ \ \
| | * | | Fix a typo in the reference manualGravatar Jason Gross2016-09-07
| |/ / / |/| | |
* | | | plugin micromega : nra also handles non-linear rational arithmetic over Q (Fi...Gravatar Frédéric Besson2016-08-30
* | | | update Proof General URLGravatar Paul Steckler2016-08-23
* | | | Documenting "Set Structural Injection".Gravatar Hugo Herbelin2016-08-21
| * | | Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
* | | | In docs, fix command to reset Ltac profilingGravatar Paul Steckler2016-08-17
|/ / /
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\| |
| * | Fix documentation typo (bug #4994).Gravatar Guillaume Melquiond2016-08-04
* | | More examples of recursive notations, with emphasis in reference manual.Gravatar Hugo Herbelin2016-07-17
* | | Fix #4793: Coq 8.6 should accept -compat 8.6Gravatar Maxime Dénès2016-07-06
* | | 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
* | Fixes in documentation.Gravatar Matthieu Sozeau2016-06-29
* | Program: cleanup in cases, add optionsGravatar Matthieu Sozeau2016-06-29
* | Merge remote-tracking branch 'github/pr/207' into trunkGravatar Maxime Dénès2016-06-28
|\ \
* | | Documenting the "only printing" notation flag.Gravatar Pierre-Marie Pédrot2016-06-28
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\ \ \ | | |/ | |/|
* | | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
| * | Reference Manual / Extraction: the original example command no longer works w...Gravatar Matej Kosik2016-06-20
| | * Add [Unset Printing Dependent Evars Line]Gravatar Jason Gross2016-06-19
| |/ |/|
* | par: like all: but in parallelGravatar Enrico Tassi2016-06-17
* | Document new Hint Mode option.Gravatar Matthieu Sozeau2016-06-16
* | Revise syntax of Hint CutGravatar Matthieu Sozeau2016-06-16
* | Merge 'pr/191' into trunkGravatar Enrico Tassi2016-06-16
|\ \
* | | typographyGravatar Matej Kosik2016-06-15
| * | Add documentation for goal selectors.Gravatar Cyprien Mangin2016-06-14