aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Merge remote-tracking branch 'github/pr/336' into v8.6Gravatar Maxime Dénès2016-11-04
|\
* | Add documentation for [Set Warnings] and the -w option.Gravatar Cyprien Mangin2016-11-04
| * 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 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.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
* | | Refolding: disable in 8.4 compat file, documentGravatar Matthieu Sozeau2016-09-12
* | | 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
* | | 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
* | | -async-proofs-delegation-threshold default value set to 0.03Gravatar Enrico Tassi2016-06-14
* | | Merge remote-tracking branch 'origin/pr/173' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \ | |/ / |/| |
* | | Merge branch "LtacProf for trunk" (PR #165).Gravatar Pierre-Marie Pédrot2016-06-14
|\ \ \
* | | | Univs: more robust Universe/Constraint decls #4816Gravatar Matthieu Sozeau2016-06-13