| Commit message (Expand) | Author | Age |
* | Revising r16550 about providing intro patterns for applying injection: | herbelin | 2013-07-09 |
* | Documenting a potential source of incompleteness in the ring tactic, | amahboub | 2013-06-17 |
* | Fixing #3056 | ppedrot | 2013-06-06 |
* | Document changes and add missing documentation for Program options. | msozeau | 2013-06-06 |
* | Start documenting new [rewrite_strat] tactic that applies rewriting | msozeau | 2013-06-04 |
* | Making the behavior of "injection ... as ..." more natural: | herbelin | 2013-06-02 |
* | Fixing a typo in the documentation of discriminate. | herbelin | 2013-06-02 |
* | Documenting the "appcontext" by default. | ppedrot | 2013-05-29 |
* | Documenting the previous commit. | ppedrot | 2013-05-12 |
* | Fix typo in manual | gareuselesinge | 2013-05-06 |
* | Renaming SearchAbout into Search and Search into SearchHead. | herbelin | 2013-04-17 |
* | Small doc fix : module subtyping cannot force access of opaques | letouzey | 2013-04-04 |
* | Revised infrastructure for lazy loading of opaque proofs | letouzey | 2013-04-02 |
* | Typo in refman (fix #2962) | letouzey | 2013-03-25 |
* | 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-21 |
* | Allowing (Co)Fixpoint to be defined local and Let-style. | ppedrot | 2013-03-11 |
* | Documentation of the "Local Definition" command. | ppedrot | 2013-03-11 |
* | Added missing documentation of Set Printing Existential Instances. | herbelin | 2013-02-21 |
* | Documenting the 'Printing Transparent/All Dependencies' command. | ppedrot | 2012-10-30 |
* | RefMan-tac: fix a few glitches concerning the documentation of eqn: | letouzey | 2012-10-23 |
* | 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-16 |
* | Port rewrites of tactic documentation from branch 8.4. | gmelquio | 2012-09-15 |
* | Obsolete syntax in documentation of Solve Obligation commands. | ppedrot | 2012-09-05 |
* | Add option Set/Unset Extraction Conservative Types. | aspiwack | 2012-08-24 |
* | Extraction: document Separate Extraction and KeepSingleton | letouzey | 2012-08-23 |
* | 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-11 |
* | Documenting eta-conversion. | herbelin | 2012-08-08 |
* | More standard layout for \lambda in chapter CIC. | herbelin | 2012-08-08 |
* | Typo in r15654 | herbelin | 2012-08-07 |
* | Updating credits for final 8.4 | herbelin | 2012-08-07 |
* | Document the command Add/Remove Search Blacklist | letouzey | 2012-08-03 |
* | documentation of bullets (forward port from v8.4). | courtieu | 2012-07-25 |
* | 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-09 |
* | 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-07-05 |
* | Fixed #2789. | ppedrot | 2012-05-25 |
* | 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-10 |
* | 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-05-08 |
* | Removed the quasi-useless gtk2rc file and the documentation that went with it... | ppedrot | 2012-04-27 |