aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
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-03-03Adding explicitly a file to work in the context of propositional extensionality.Hugo Herbelin
2017-03-03Adding a file providing extensional choice (i.e. choice over setoids).Hugo Herbelin
2017-03-03Logic library: Adding a characterization of excluded-middle in term ofHugo Herbelin
2017-02-20Fix V7 syntax in refman.Théo Zimmermann
2017-01-19Merge branch 'v8.6'Pierre-Marie Pédrot
2016-12-28Fix some typos in tutorial (bug #5294).Guillaume Melquiond
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-12-02Merge remote-tracking branch 'github/pr/364' into v8.6Maxime Dénès
2016-11-30Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-30Update copyright on documentation cover.Maxime Dénès
2016-11-24Fix some documentation typos.Guillaume Melquiond
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
2016-11-05Minor fix in documentationMatthieu Sozeau
2016-11-04Merge remote-tracking branch 'github/pr/336' into v8.6Maxime Dénès
2016-11-04Add documentation for [Set Warnings] and the -w option.Cyprien Mangin
2016-11-03Do not shelve non-class subgoals but fail, it shouldMatthieu Sozeau
2016-11-03typeclasses eauto Implem/doc of shelving strategyMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 02:26:32 +0000