| Age | Commit message (Expand) | Author |
|---|
| 2013-06-17 | Documenting a potential source of incompleteness in the ring tactic, | amahboub |
| 2013-06-06 | Fixing #3056 | ppedrot |
| 2013-06-06 | Document changes and add missing documentation for Program options. | msozeau |
| 2013-06-04 | Start documenting new [rewrite_strat] tactic that applies rewriting | msozeau |
| 2013-06-02 | Making the behavior of "injection ... as ..." more natural: | herbelin |
| 2013-06-02 | Fixing a typo in the documentation of discriminate. | herbelin |
| 2013-05-29 | Documenting the "appcontext" by default. | ppedrot |
| 2013-05-12 | Documenting the previous commit. | ppedrot |
| 2013-05-06 | Fix typo in manual | gareuselesinge |
| 2013-04-17 | Renaming SearchAbout into Search and Search into SearchHead. | herbelin |
| 2013-04-04 | Small doc fix : module subtyping cannot force access of opaques | letouzey |
| 2013-04-02 | Revised infrastructure for lazy loading of opaque proofs | letouzey |
| 2013-03-25 | Typo in refman (fix #2962) | letouzey |
| 2013-03-21 | Using hnf instead of "intro H" for forcing reduction to a product. | herbelin |
| 2013-03-21 | Fixing an old pecularity of "red": head betaiota redexes are now | herbelin |
| 2013-03-11 | Allowing (Co)Fixpoint to be defined local and Let-style. | ppedrot |
| 2013-03-11 | Documentation of the "Local Definition" command. | ppedrot |
| 2013-02-21 | Added missing documentation of Set Printing Existential Instances. | herbelin |
| 2012-10-30 | Documenting the 'Printing Transparent/All Dependencies' command. | ppedrot |
| 2012-10-23 | RefMan-tac: fix a few glitches concerning the documentation of eqn: | letouzey |
| 2012-09-16 | Move reflexivity, symmetry, and transitivity, next to f_equal, in the documen... | gmelquio |
| 2012-09-16 | Some more fixes to tactic documentation. | gmelquio |
| 2012-09-16 | Beautify tactic documentation a bit more. | gmelquio |
| 2012-09-16 | Remove superfluous spaces and commas in tactic documentation. | gmelquio |
| 2012-09-16 | Fix index generation for the pdf document. | gmelquio |
| 2012-09-15 | Port rewrites of tactic documentation from branch 8.4. | gmelquio |
| 2012-09-05 | Obsolete syntax in documentation of Solve Obligation commands. | ppedrot |
| 2012-08-24 | Add option Set/Unset Extraction Conservative Types. | aspiwack |
| 2012-08-23 | Extraction: document Separate Extraction and KeepSingleton | letouzey |
| 2012-08-11 | Improving rendering of ldots in doc (partially done, there are too | herbelin |
| 2012-08-11 | Added support for option Local (at module level) in Tactic Notation. | herbelin |
| 2012-08-11 | Improving rendering of ...-separated lists and sequences in reference | herbelin |
| 2012-08-08 | Documenting eta-conversion. | herbelin |
| 2012-08-08 | More standard layout for \lambda in chapter CIC. | herbelin |
| 2012-08-07 | Typo in r15654 | herbelin |
| 2012-08-07 | Updating credits for final 8.4 | herbelin |
| 2012-08-03 | Document the command Add/Remove Search Blacklist | letouzey |
| 2012-07-25 | documentation of bullets (forward port from v8.4). | courtieu |
| 2012-07-09 | The tactic remember now accepts a final eqn:H option (grant wish #2489) | letouzey |
| 2012-07-09 | induction/destruct : nicer syntax for generating equations (solves #2741) | letouzey |
| 2012-07-05 | Legacy Ring and Legacy Field migrated to contribs | letouzey |
| 2012-07-05 | Open Local Scope ---> Local Open Scope, same with Notation and alii | letouzey |
| 2012-07-05 | ZArith + other : favor the use of modern names instead of compat notations | letouzey |
| 2012-05-25 | Fixed #2789. | ppedrot |
| 2012-05-10 | Addedum to documentation of bullets: I now use the dedicated coq_example | aspiwack |
| 2012-05-10 | Documentation for Unfocused, braces and bullets. | aspiwack |
| 2012-05-08 | Rephrasing section on Sorts in CIC chapter, accordingly to discussions | herbelin |
| 2012-05-08 | Ref. man., ch. CIC: clarifying the redundancy coming from having both | herbelin |
| 2012-04-27 | Removed the quasi-useless gtk2rc file and the documentation that went with it... | ppedrot |
| 2012-04-13 | Uniformisation in the documentation: remove the use of 'coinductive' in | aspiwack |
