aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2012-06-12make sure that documentation compilation works after adding files forbertot
2012-05-29place all files specific to camlp4 syntax extensions in grammar/letouzey
2012-05-25Fixed #2789.ppedrot
2012-05-10Addedum to documentation of bullets: I now use the dedicated coq_exampleaspiwack
2012-05-10Documentation for Unfocused, braces and bullets.aspiwack
2012-05-08Rephrasing section on Sorts in CIC chapter, accordingly to discussionsherbelin
2012-05-08Ref. man., ch. CIC: clarifying the redundancy coming from having bothherbelin
2012-05-03Fixup r15251 second timepboutill
2012-04-27Removed the quasi-useless gtk2rc file and the documentation that went with it...ppedrot
2012-04-13MSetRBT : implementation of MSets via Red-Black treesletouzey
2012-04-13Uniformisation in the documentation: remove the use of 'coinductive' inaspiwack
2012-04-13Documentation of records defined with the keywords Inductive andaspiwack
2012-04-13Restores pdf bookmarks in the reference manual.aspiwack
2012-04-12lib directory is cut in 2 cma.pboutill
2012-03-26Slight change in the semantics of arguments scopes: scopes can noherbelin
2012-03-23Documentation of last commit concerning Backtrackingletouzey
2012-03-23Remove old proof-managment commands Suspend/Resumeletouzey
2012-03-19RefMan: Environment variables description updatepboutill
2012-02-29RefMan update about match syntax.pboutill
2012-02-20- changing minimal version for OCaml: Coq uses Filename.dirsep that is availa...notin
2012-02-18Document the [unify] tactic.msozeau
2012-02-07Documentation for Grab Existential Variables.aspiwack
2012-02-01Corrected a careless cut-and-paste in Gallina description which dated back to...ppedrot
2012-02-01Improved synchronisation of stdlib index page with current library state.herbelin
2012-01-31index-list.html.template: add missing filespboutill
2012-01-21Coqtop and coqc: cleaning description of options in RefMan and manpages.pboutill
2012-01-20Added documentation for "r foo" in Ltac debugger.herbelin
2012-01-20Added documentation for "Set Parsing Explicit" + fixed mistakenlyherbelin
2012-01-19Added the btauto tactic to the documentation.ppedrot
2011-12-26Reference Manual: misc fixes (spelling, index, updating pre-8.0 syntax).herbelin
2011-12-25Version number, copyright, credits: missing updates.herbelin
2011-12-23Credits for 8.4: More exhaustive list of external contributors.herbelin
2011-12-22Credits for 8.4 + resetting COMPATIBILITY file.herbelin
2011-12-18Fixed a Not_found bug when declaring in a section some implicitherbelin
2011-12-17Command Arguments: standardizing format of error messages and American spelling.herbelin
2011-12-12Proof using ...gareuselesinge
2011-12-07Html page titlespboutill
2011-12-06Documentation of Arguments + implicitsgareuselesinge
2011-12-06Documentation for Arguments + notation scopesgareuselesinge
2011-12-06Documentation for Arguments + simplgareuselesinge
2011-12-04Fixing bugs in doc about when "with" is needed or not to give bindingsherbelin
2011-11-29Documentation of appcontextletouzey
2011-11-28doc: two minor fixes to make my latex happyletouzey
2011-11-21/home/pirbo/.coqrc* are read againpboutill
2011-11-21-user option removalpboutill
2011-11-20coqrc in the right XDG_CONFIG_HOME/coq folderpboutill
2011-11-20CoqIdE configuration file won't pollute your home anymorepboutill
2011-11-20Add support for XDG_DATA_HOME and XDG_DATA_DIRS.pboutill
2011-10-18Extraction.tex: typo in an Extract Inductive example (fix #2625)letouzey
2011-10-09mainbiblio.bib : get rid of merge marker from failed mergeletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 11:04:23 +0000