aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
AgeCommit message (Expand)Author
2013-05-29Documenting the "appcontext" by default.ppedrot
2013-05-12Documenting the previous commit.ppedrot
2013-05-06Fix typo in manualgareuselesinge
2013-04-17Renaming SearchAbout into Search and Search into SearchHead.herbelin
2013-04-04Small doc fix : module subtyping cannot force access of opaquesletouzey
2013-04-02Revised infrastructure for lazy loading of opaque proofsletouzey
2013-03-25Typo in refman (fix #2962)letouzey
2013-03-21Using hnf instead of "intro H" for forcing reduction to a product.herbelin
2013-03-21Fixing an old pecularity of "red": head betaiota redexes are nowherbelin
2013-03-11Allowing (Co)Fixpoint to be defined local and Let-style.ppedrot
2013-03-11Documentation of the "Local Definition" command.ppedrot
2013-02-21Added missing documentation of Set Printing Existential Instances.herbelin
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-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-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-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-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-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-04-27Removed the quasi-useless gtk2rc file and the documentation that went with it...ppedrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 10:28:22 +0000