aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
AgeCommit message (Expand)Author
2017-06-14Merge PR#765: Remove obsolete Show commandsMaxime Dénès
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
2017-06-12Remove commented documentation for Show Tree.Théo Zimmermann
2017-06-01Merge PR#449: make specialize smarter (bug 5370).Maxime Dénès
2017-05-31Documenting the new behaviour of specialize.Pierre Courtieu
2017-05-30Documentation for eassert, eenough, epose proof, eset, eremember, epose.Hugo Herbelin
2017-05-27Documenting the existence of first and solve as Ltac definitions.Pierre-Marie Pédrot
2017-05-25Merge PR#406: coq makefile2Maxime Dénès
2017-05-23add the only targetEnrico Tassi
2017-05-23enters coq_makefile2Enrico Tassi
2017-05-23[vernac] Remove `Save thm id.` command.Emilio Jesus Gallego Arias
2017-05-23[vernac] Remove `Save.` command.Emilio Jesus Gallego Arias
2017-05-17Documenting relaxing of constraints on injection.Hugo Herbelin
2017-05-17Merge PR#457: Adding an even more compact goal hyps mode.Maxime Dénès
2017-05-17Merge branch 'v8.6'Pierre-Marie Pédrot
2017-05-11Add documentation for Set Ltac Batch DebugJason Gross
2017-05-11Documenting Printing Compact Contexts + CHANGESPierre Courtieu
2017-05-11Merge PR#201: Transparent abstractMaxime Dénès
2017-05-04Improve documentation of assert / pose proof / specialize.Théo Zimmermann
2017-05-03Merge PR#411: Mention template polymorphism in the documentation.Maxime Dénès
2017-05-03Fix outdated description in RefMan.Théo Zimmermann
2017-05-01More consistent writing of de Bruijn.Théo Zimmermann
2017-05-01Fix for bug 5507. Mispelt de Bruijn.Théo Zimmermann
2017-04-28Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Maxime Dénès
2017-04-27fix order of command-line arguments mentioned in Add LoadPathPaul Steckler
2017-04-25Mark transparent_abstract as risky in docsJason Gross
2017-04-25Add transparent_abstract tacticJason Gross
2017-04-24refman: remember the old name of template polymorphism.Gaetan Gilbert
2017-04-12Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...Maxime Dénès
2017-04-11Update RefMan-pre to mention template polymorphism.Gaetan Gilbert
2017-04-11Use "template polymorphism" in the documentation.Gaetan Gilbert
2017-04-11Mention template polymorphism in the documentation.Gaetan Gilbert
2017-04-09Merge PR#460: Turning the printing primitive projection compatibility flag of...Maxime Dénès
2017-04-09Fixing #5420 as well as many related bugs due to miscounting let-ins.Hugo Herbelin
2017-04-07Merge PR#485: Document Show MatchMaxime Dénès
2017-04-07Turning the printing primitive projection parameter flag off by default.Hugo Herbelin
2017-04-07Turning the printing primitive projection compatibility flag off by default.Hugo Herbelin
2017-04-06Merge PR#455: Farewell decl_modeMaxime Dénès
2017-03-23Documenting the grammar {| ... |} syntax for building records.Hugo Herbelin
2017-03-23Merge PR#433: doc: fix a French-ismMaxime Dénès
2017-03-22Fix some typos.Guillaume Melquiond
2017-03-22Merge PR#482: [toplevel] Remove unusable option -notopMaxime Dénès
2017-03-17Document Show Match, add ref to that in match variants/extensionsPaul Steckler
2017-03-14doc: fix a French-ismValentin Robert
2017-03-14[toplevel] Remove unusable option -notopEmilio Jesus Gallego Arias
2017-03-14Merge PR#438: Fix V7 syntax in refman.Maxime Dénès
2017-03-09Typo doc notations.Hugo Herbelin
2017-03-09Clarifying doc about interpretation of scopes in notations (#5386).Hugo Herbelin
2017-03-07Farewell decl_modeEnrico Tassi
2017-02-20Fix V7 syntax in refman.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:41:45 +0000