aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Add documentation for Set Ltac Batch DebugGravatar Jason Gross2017-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
|\ \
* | | 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
|\ \ \
| | | * 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
| |\
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-30
|\| |
| * | Update copyright on documentation cover.Gravatar Maxime Dénès2016-11-30
| * | Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\| |
| | * Add missing label. Fixes broken ref.Gravatar Théo Zimmermann2016-11-17
| |/
| * Revert more of a477dc for good measureGravatar Matthieu Sozeau2016-11-16