| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-02-05 | Fix some documentation typos. | Guillaume Melquiond | |
| 2015-01-29 | Fix index of reference manual. | Guillaume Melquiond | |
| 2015-01-29 | Remove spurious "Loading ML file" and "<W> Grammar extension" from the ↵ | Guillaume Melquiond | |
| reference manual. | |||
| 2015-01-29 | Remove some "Warning:" from the reference manual. | Guillaume Melquiond | |
| 2015-01-29 | Fix some typos in the documentation. | Guillaume Melquiond | |
| 2015-01-29 | Fix some broken Coq scripts in the reference manual. | Guillaume Melquiond | |
| 2015-01-27 | Doc: Overfull lines in chapter on Canonical Structures. | Hugo Herbelin | |
| 2015-01-24 | Doc: Fixing some compilation problems with chapter Canonical | Hugo Herbelin | |
| Structures. Text mode + a "Require Import" in a module which provokes suspect warnings "Exception Not_found". | |||
| 2015-01-24 | Reference Manual: Documenting new printing of evars and new effect of | Hugo Herbelin | |
| Set Printing Existential Instances (see bug report #3951). | |||
| 2015-01-21 | Reference Manual/Credits: expand the paragraph on the new proof engine to ↵ | Arnaud Spiwack | |
| match the overall style. | |||
| 2015-01-21 | Reference Manual/Credits: native compute is a major contribution. | Arnaud Spiwack | |
| It is, at the very least, listed as such in the overview. So, I moved it to the relevant part and expanded the description with a sentence or two. | |||
| 2015-01-21 | Reference manual/Credits: populate the "various smaller-scale improvements" ↵ | Arnaud Spiwack | |
| part. | |||
| 2015-01-21 | Reference Manual/Credits: remove a duplicate. | Arnaud Spiwack | |
| 2015-01-21 | Reference manual: pass over the credit section for English. | Arnaud Spiwack | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |