aboutsummaryrefslogtreecommitdiff
path: root/doc/common
AgeCommit message (Expand)Author
2020-04-20Remove coqremote stylesheets which were useless since the Sphinx migration.Théo Zimmermann
2019-06-17Update copyright years outside of headers.Théo Zimmermann
2019-05-21Fixing typos - Part 1JPR
2019-03-14Documentation for SPropGaëtan Gilbert
2019-02-21Stdlib HTML documentation: fix a few absolute URLsVincent Laporte
2019-01-29Use \mathcal instead of \calGaëtan Gilbert
2018-02-20Extended documentation for notations referring to binders.Hugo Herbelin
2017-11-25Updating the current official writing of OCaml, updating Camlp4->Camlp5.Hugo Herbelin
2017-10-25Put newlines at the end of files.Gaëtan Gilbert
2017-10-06Fix copyright info in reference manual.Théo Zimmermann
2017-08-23Update coypright dates on documentationMatthieu Sozeau
2017-08-02Port ssr manual to Coq's latex/hevea styleEnrico Tassi
2017-08-02Makefile.doc: implement serve-refman-8080 targetEnrico Tassi
2017-03-23Documenting the grammar {| ... |} syntax for building records.Hugo Herbelin
2016-12-06Fix broken documentation in presence of \zeroone{... \tt ...}.Guillaume Melquiond
2016-11-30Update copyright on documentation cover.Maxime Dénès
2016-04-24Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-12FIX: HTML version of Chapter 4 of the Reference ManualMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-14Updating and improving the documentation of intros patterns.Hugo Herbelin
2015-12-10ENH: examples for 'strict positivity' were expandedMatej Kosik
2015-12-10CLEANUP: s/List_A/List~A/gMatej Kosik
2015-12-10CLEANUP: superfluous examples were removedMatej Kosik
2015-12-10ENH: new example: "even"Matej Kosik
2015-12-10ALPHA-CONVERSION: s/Length/has_length/gMatej Kosik
2015-12-10ENH: The beginning of Section 4.5 (Inductive declarations) was changed in ord...Matej Kosik
2015-12-10RefMan, ch. 4: Removing the local context of inductive definitions.Hugo Herbelin
2015-12-10RefMan, ch. 4: Adding discharging of inductive types.Hugo Herbelin
2015-12-10RefMan, ch. 4: In chapter 4 about CIC, renounced to keep a localHugo Herbelin
2015-12-10RefMan, ch. 4: Reformulating introduction of the chapter on CIC, beingHugo Herbelin
2015-07-31Remove some outdated files and fix permissions.Guillaume Melquiond
2015-02-17Separate index for vernacular options.Maxime Dénès
2015-01-13Refresh some copyright headers.Maxime Dénès
2015-01-05Added more informative messages about bullets.Pierre Courtieu
2014-12-09refman: switch all source files to utf8Pierre Letouzey
2014-12-09refman: remove ?uri=referer in urls pointing to validator.w3.orgPierre Letouzey
2014-12-09refman: xhtml validity of the cover pagePierre Letouzey
2014-12-09doc: improved xhtml compatibility (cover, header,...)Pierre Letouzey
2014-12-09doc/stdlib: fix the html charset in header.html and coPierre Letouzey
2014-12-09doc: version number in cover.html + updates in coq.inria.fr stylePierre Letouzey
2014-12-09Port to trunk commit r16062 of v8.4 (Correction des entêtes pour la document...notin
2014-12-09Port to trunk the old commit r14895 of v8.4 (styles for the stdlib documentat...notin
2014-11-07doc: version number in cover.html + updates in coq.inria.fr stylePierre Letouzey
2014-08-05Making references to Proof General and CoqIDE uniform in Reference Manual.Hugo Herbelin
2012-09-16Beautify tactic documentation a bit more.gmelquio
2012-09-16Remove superfluous spaces and commas in tactic documentation.gmelquio
2012-08-11Improving rendering of ldots in doc (partially done, there are tooherbelin
2012-08-11Added support for option Local (at module level) in Tactic Notation.herbelin
2012-08-11Improving rendering of ...-separated lists and sequences in referenceherbelin