| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-01-21 | Reference manual: fix typo in doc of [tryif/then/else]. | Arnaud Spiwack | |
| Fixes #3939. | |||
| 2015-01-17 | Univs: Complete documentation in refman. | Matthieu Sozeau | |
| 2015-01-15 | Minor fixes to the refman credits to be continued. | Matthieu Sozeau | |
| 2015-01-15 | Move explanations about primitive projections to the manual. | Matthieu Sozeau | |
| 2015-01-15 | Expand Credits for 8.5 and doc on universes | Matthieu Sozeau | |
| 2015-01-15 | Tentatively updating credits while remaining brief. | Hugo Herbelin | |
| 2015-01-14 | Reference manual: I had previously omitted the syntax entry for [> t1|…|tn]. | Arnaud Spiwack | |
| 2015-01-14 | Reference manual: document tryif/then/else. | Arnaud Spiwack | |
| 2015-01-14 | Reference manual: document multimatch. | Arnaud Spiwack | |
| 2015-01-14 | Reference manual: try and improve documentation for Ltac's match. | Arnaud Spiwack | |
| In particular document the "once" behaviour. | |||
| 2015-01-14 | Reference manual: try and improve the documentation of lazymatch. | Arnaud Spiwack | |
| In particular try to avoid the use of the word "backtracking" which refers to too many things. | |||
| 2015-01-14 | Reference manual: document gfail. | Arnaud Spiwack | |
| 2015-01-13 | Refresh some copyright headers. | Maxime Dénès | |
| 2015-01-13 | More documentation of the Local Definitions and Axioms. | Pierre-Marie Pédrot | |
| 2015-01-12 | Whodidwhat-8.5: a global pass | Arnaud Spiwack | |
| Updating my own work and others when I could think of them. | |||
| 2015-01-12 | whodidwhat-8.5: typo. | Arnaud Spiwack | |
| 2015-01-11 | some credits for STM | Enrico Tassi | |
| 2015-01-08 | Start credits for 8.5. | Matthieu Sozeau | |
| 2015-01-08 | Small fix in whodidwhat 8.5. | Pierre Courtieu | |
| 2015-01-08 | Fixed and extend bullet related info/error messages. + doc. | Pierre Courtieu | |
| Had to put some hook in the handler of Proofview.NoSuchgoals. Documentation updated. CHANGE updated. | |||
| 2015-01-08 | Fix some documentation typos. | Guillaume Melquiond | |
| 2015-01-08 | Add a few words in whodidwhat. | Maxime Dénès | |
| 2015-01-08 | Document native_compute. | Maxime Dénès | |
| 2015-01-07 | Initiating who-did-what for 8.5 | Hugo Herbelin | |
| 2015-01-07 | Committing whodidwhat files. | Hugo Herbelin | |
| 2015-01-06 | rename: vi -> vio | Enrico Tassi | |
| 2015-01-06 | Fix some documentation typos. | Guillaume Melquiond | |
| 2015-01-05 | Added more informative messages about bullets. | Pierre Courtieu | |
| Updated doc, but not tests-suite yet. | |||
| 2015-01-05 | Updating documentation about bullets. | Pierre Courtieu | |
| Error messages were outdated. | |||
| 2014-12-30 | Document the new behavior of lazymatch. | Guillaume Melquiond | |
| 2014-12-25 | Document 6d5b56d971 (forbid Require inside modules). | Maxime Dénès | |
| 2014-12-19 | Better doc and a few fixes for Proof using. | Enrico Tassi | |
| 2014-12-18 | Proof using: New vernacular to name sets of section variables | Enrico Tassi | |
| 2014-12-12 | Searchxxx now search also the hypothesis and support goal selector. | Pierre Courtieu | |
| Documentation also updated. | |||
| 2014-12-09 | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey | |
| 2014-12-09 | refman: switch all source files to utf8 | Pierre Letouzey | |
| Putting utf8 everywhere helps the maintainance of the online refman. And anyway, this is the way to go. We should also chase and migrate the few remaining iso-latin-1 files elsewhere in the sources. | |||
| 2014-12-09 | refman: fix broken urls | Pierre Letouzey | |
| 2014-12-09 | refman: remove ?uri=referer in urls pointing to validator.w3.org | Pierre Letouzey | |
| Unfortunately, these ?uri=referer parameters do not work correctly now that coq.inria.fr forces the switch to https before answering any document. See: http://validator.w3.org/docs/help.html#faq-referer I currently see no workaround for that, apart from generating links like ?uri=http://the.real.url/of/my/page, which would be quite painful. For now, users interested in checking the validity of our pages will have to copy-paste the url they want to check after clicking on the validator button. | |||
| 2014-12-09 | refman/Omega.tex: do not advertize Pierre Cregut's email for bug reports | Pierre Letouzey | |
| 2014-12-09 | refman/coqdoc.tex: fix two erroneous \url | Pierre Letouzey | |
| 2014-12-09 | refman: for xhtml validity, add 'alt' attributes to img | Pierre Letouzey | |
| 2014-12-09 | refman: avoid label names with whitespace (unsupported in html) | Pierre Letouzey | |
| 2014-12-09 | refman: xhtml validity of the cover page | Pierre Letouzey | |
| 2014-12-09 | doc/stdlib: fix the xhtml validity of the index-list template | Pierre Letouzey | |
| 2014-12-09 | doc: improved xhtml compatibility (cover, header,...) | Pierre Letouzey | |
| 2014-12-09 | doc/stdlib: fix the html charset in header.html and co | Pierre Letouzey | |
| 2014-12-09 | doc: version number in cover.html + updates in coq.inria.fr style | Pierre Letouzey | |
| To be continued someday, those style files are full of redundancies... | |||
| 2014-12-09 | Port to trunk commit r16062 of v8.4 (Correction des entêtes pour la ↵ | notin | |
| documentation en ligne) | |||
| 2014-12-09 | Port to trunk the old commit r14895 of v8.4 (styles for the stdlib ↵ | notin | |
| documentation) This commit r14895 comes apparently itself from commit r12010 in branch v8.2 | |||
| 2014-11-30 | Documenting the Set Refine Instance Mode. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |