aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2012-10-30Documenting the 'Printing Transparent/All Dependencies' command.ppedrot
2012-10-23RefMan-tac: fix a few glitches concerning the documentation of eqn:letouzey
2012-09-16Move reflexivity, symmetry, and transitivity, next to f_equal, in the documen...gmelquio
2012-09-16Some more fixes to tactic documentation.gmelquio
2012-09-16Beautify tactic documentation a bit more.gmelquio
2012-09-16Remove superfluous spaces and commas in tactic documentation.gmelquio
2012-09-16Fix index generation for the pdf document.gmelquio
2012-09-15Fix failure to compile doc/stdlib/Library.tex.gmelquio
2012-09-15Port rewrites of tactic documentation from branch 8.4.gmelquio
2012-09-05Obsolete syntax in documentation of Solve Obligation commands.ppedrot
2012-08-24Add option Set/Unset Extraction Conservative Types.aspiwack
2012-08-23Remove a script unused since 2006 (cf commit r8626)letouzey
2012-08-23Extraction: document Separate Extraction and KeepSingletonletouzey
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
2012-08-08Updating version numbers.herbelin
2012-08-08Documenting eta-conversion.herbelin
2012-08-08More standard layout for \lambda in chapter CIC.herbelin
2012-08-07Typo in r15654herbelin
2012-08-07Updating credits for final 8.4herbelin
2012-08-03Document the command Add/Remove Search Blacklistletouzey
2012-07-25documentation of bullets (forward port from v8.4).courtieu
2012-07-20Vector equalities first stuffpboutill
2012-07-10isolate instances about Permutation and PermutationA which may slow rewriteletouzey
2012-07-09The tactic remember now accepts a final eqn:H option (grant wish #2489)letouzey
2012-07-09induction/destruct : nicer syntax for generating equations (solves #2741)letouzey
2012-07-05Legacy Ring and Legacy Field migrated to contribsletouzey
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 17:59:56 +0000