aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Documenting relaxing of constraints on injection.Gravatar Hugo Herbelin2017-05-17
* Merge PR#457: Adding an even more compact goal hyps mode.Gravatar Maxime Dénès2017-05-17
|\
* \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-05-17
|\ \
* | | Add documentation for Set Ltac Batch DebugGravatar Jason Gross2017-05-11
| | * Documenting Printing Compact Contexts + CHANGESGravatar Pierre Courtieu2017-05-11
* | | Merge PR#201: Transparent abstractGravatar Maxime Dénès2017-05-11
|\ \ \
* | | | Improve documentation of assert / pose proof / specialize.Gravatar Théo Zimmermann2017-05-04
| |_|/ |/| |
* | | Merge PR#411: Mention template polymorphism in the documentation.Gravatar Maxime Dénès2017-05-03
|\ \ \
| | | * Fix outdated description in RefMan.Gravatar Théo Zimmermann2017-05-03
* | | | More consistent writing of de Bruijn.Gravatar Théo Zimmermann2017-05-01
* | | | Fix for bug 5507. Mispelt de Bruijn.Gravatar Théo Zimmermann2017-05-01
* | | | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Gravatar Maxime Dénès2017-04-28
|\ \ \ \
| | | | * fix order of command-line arguments mentioned in Add LoadPathGravatar Paul Steckler2017-04-27
| | | * | Mark transparent_abstract as risky in docsGravatar Jason Gross2017-04-25
| | | * | Add transparent_abstract tacticGravatar Jason Gross2017-04-25
| |_|/ / |/| | |
| | * | refman: remember the old name of template polymorphism.Gravatar Gaetan Gilbert2017-04-24
* | | | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...Gravatar Maxime Dénès2017-04-12
|\ \ \ \
| | | * | Update RefMan-pre to mention template polymorphism.Gravatar Gaetan Gilbert2017-04-11
| | | * | Use "template polymorphism" in the documentation.Gravatar Gaetan Gilbert2017-04-11
| | | * | Mention template polymorphism in the documentation.Gravatar Gaetan Gilbert2017-04-11
| |_|/ / |/| | |
* | | | Merge PR#460: Turning the printing primitive projection compatibility flag of...Gravatar Maxime Dénès2017-04-09
|\ \ \ \
| | | * | Fixing #5420 as well as many related bugs due to miscounting let-ins.Gravatar Hugo Herbelin2017-04-09
| |_|/ / |/| | |
* | | | Merge PR#485: Document Show MatchGravatar Maxime Dénès2017-04-07
|\ \ \ \
| | * | | Turning the printing primitive projection parameter flag off by default.Gravatar Hugo Herbelin2017-04-07
| | * | | Turning the printing primitive projection compatibility flag off by default.Gravatar Hugo Herbelin2017-04-07
| |/ / / |/| | |
* | | | Merge PR#455: Farewell decl_modeGravatar Maxime Dénès2017-04-06
|\ \ \ \
| | | * | Documenting the grammar {| ... |} syntax for building records.Gravatar Hugo Herbelin2017-03-23
| |_|/ / |/| | |
* | | | Merge PR#433: doc: fix a French-ismGravatar Maxime Dénès2017-03-23
|\ \ \ \
* | | | | Fix some typos.Gravatar Guillaume Melquiond2017-03-22
* | | | | Merge PR#482: [toplevel] Remove unusable option -notopGravatar Maxime Dénès2017-03-22
|\ \ \ \ \
| | | | * | Document Show Match, add ref to that in match variants/extensionsGravatar Paul Steckler2017-03-17
| |_|_|/ / |/| | | |
| | * | | doc: fix a French-ismGravatar Valentin Robert2017-03-14
| * | | | [toplevel] Remove unusable option -notopGravatar Emilio Jesus Gallego Arias2017-03-14
* | | | | Merge PR#438: Fix V7 syntax in refman.Gravatar Maxime Dénès2017-03-14
|\ \ \ \ \ | |/ / / / |/| | | |
* | | | | Typo doc notations.Gravatar Hugo Herbelin2017-03-09
* | | | | Clarifying doc about interpretation of scopes in notations (#5386).Gravatar Hugo Herbelin2017-03-09
| | | * | Farewell decl_modeGravatar Enrico Tassi2017-03-07
| | |/ /
* | | | Adding explicitly a file to work in the context of propositional extensionality.Gravatar Hugo Herbelin2017-03-03
* | | | Adding a file providing extensional choice (i.e. choice over setoids).Gravatar Hugo Herbelin2017-03-03
* | | | Logic library: Adding a characterization of excluded-middle in term ofGravatar Hugo Herbelin2017-03-03
| |/ / |/| |
| * | Fix V7 syntax in refman.Gravatar Théo Zimmermann2017-02-20
|/ /
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-01-19
|\|
| * Fix some typos in tutorial (bug #5294).Gravatar Guillaume Melquiond2016-12-28
| * Fix incorrect documentation that prevents successful compilation (bug #5265).Gravatar Guillaume Melquiond2016-12-16
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
|\|
| * Fix broken documentation in presence of \zeroone{... \tt ...}.Gravatar Guillaume Melquiond2016-12-06
| * Update documentation (bugs #5246 and #5251).Gravatar Guillaume Melquiond2016-12-06
| * Change module for Coq loopGravatar Paul Steckler2016-12-05
| * the -byte option is deprecatedGravatar Paul Steckler2016-12-05
| * Merge remote-tracking branch 'github/pr/364' into v8.6Gravatar Maxime Dénès2016-12-02
| |\