aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
* BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-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 the existence of first and solve as Ltac definitions.Gravatar Pierre-Marie Pédrot2017-05-27
* Merge PR#406: coq makefile2Gravatar Maxime Dénès2017-05-25
|\
| * add the only targetGravatar Enrico Tassi2017-05-23
| * enters coq_makefile2Gravatar Enrico Tassi2017-05-23
* | [vernac] Remove `Save thm id.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
* | [vernac] Remove `Save.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
|/
* 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