aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
AgeCommit message (Expand)Author
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
2017-01-19Merge branch 'v8.6'Pierre-Marie Pédrot
2016-12-16Fix incorrect documentation that prevents successful compilation (bug #5265).Guillaume Melquiond
2016-12-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-12-06Fix broken documentation in presence of \zeroone{... \tt ...}.Guillaume Melquiond
2016-12-06Update documentation (bugs #5246 and #5251).Guillaume Melquiond
2016-12-05Change module for Coq loopPaul Steckler
2016-12-05the -byte option is deprecatedPaul Steckler
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-17Add missing label. Fixes broken ref.Théo Zimmermann
2016-11-16Revert more of a477dc for good measureMatthieu Sozeau
2016-11-15Revert part of a477dc, disallow_shelvedMatthieu Sozeau
2016-11-14Do not mention "none" in warnings doc, as it is there for compatibility.Maxime Dénès
2016-11-10Update CHANGES and credits for 8.6beta1.Maxime Dénès
2016-11-08Merge remote-tracking branch 'github/pr/348' into v8.6Maxime Dénès
2016-11-08Update documentation of Arguments after recent changes.Maxime Dénès
2016-11-08Rewording from EnricoMatthieu Sozeau
2016-11-07After Emilio's comment.Matthieu Sozeau
2016-11-07Merge remote-tracking branch 'github/pr/339' into v8.6Maxime Dénès
2016-11-07Document two new variants of refineMatthieu Sozeau
2016-11-07More accurate contributor list.Matthieu Sozeau
2016-11-07Hugo and Maxime's 2nd pass of commentsMatthieu Sozeau
2016-11-06Hugo's commentsMatthieu Sozeau
2016-11-06Maxime's commentsMatthieu Sozeau
2016-11-06Fixes from Enrico's reviewMatthieu Sozeau
2016-11-05Credits for 8.6Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 06:29:37 +0000