| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2014-11-27 | FAQ: fix some broken urls | Pierre Letouzey | |
| 2014-11-27 | typos | Enrico Tassi | |
| 2014-11-17 | Documenting the -color option. | Pierre-Marie Pédrot | |
| 2014-11-17 | Documenting use of colors in Coq. | Pierre-Marie Pédrot | |
| 2014-11-16 | Enforcing a stronger difference between the two syntaxes "simpl | Hugo Herbelin | |
| reference" and "simpl pattern" in the code (maybe we should have merged them instead, but I finally decided to enforce their difference, even if some compatibility is to be preversed - the idea is that at some time "simpl reference" would only call a weak-head simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n) rather than S(S(n)) which could be useful for better using induction hypotheses. In the process we also implement the following: - 'simpl "+"' is accepted to reduce all applicative subterms whose head symbol is written "+" (in the toplevel scope); idem for vm_compute and native_compute - 'simpl reference' works even if reference has maximally inserted implicit arguments (this solves the "simpl fst" incompatibility) - compatibility of ltac expressions referring to vm_compute and native_compute with functor application should now work (i.e. vm_compute and native_compute are now taken into account in tacsubst.ml) - for compatibility, "simpl eq" (assuming no maximal implicit args in eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed. By the way, is "mul" on nat defined optimally? "3*n" simplifies to "n+(n+(n+0))". Are there some advantages of this compared to have it simplified to "n+n+n" (i.e. to "(n+n)+n"). | |||
| 2014-11-12 | Document (some) Proof using syntax + the new Optimize commands | Enrico Tassi | |
| 2014-11-07 | Fixing doc of Functional Induction. | Hugo Herbelin | |
| 2014-11-07 | doc: version number in cover.html + updates in coq.inria.fr style | Pierre Letouzey | |
| 2014-11-04 | Documenting the change of semantics of the replace tactic. | Pierre-Marie Pédrot | |
| 2014-11-01 | Document [Info] command. | Arnaud Spiwack | |
| 2014-10-27 | Use the url package, since coqdoc generates \url commands. | Guillaume Melquiond | |
| 2014-10-24 | Addressing report #3279 (inconsistency of behavior of the -> and <- | Hugo Herbelin | |
| introduction patterns). Whether we call -> and <- from assert as or apply in as, or as a component of a larger introduction pattern, the new documented semantics is: - behave as subst if an equation rewriting a variable (rewrite in conclusion and hyps and erase variable and hyp). - rewrite in concl if an equation not rewrite a variable or a quantified equality, then erase the hypothesis. This is potential source of incompatibilities. | |||
| 2014-10-24 | Fix typo in documentation of the [repeat] tactical. | Arnaud Spiwack | |
| Closes #3761. | |||
| 2014-10-22 | Move 'Arguments: clear implicits' to 2.7.4 (Close 2891) | Enrico Tassi | |
| 2014-10-16 | More fallout from elisp rename | Anders Kaseorg | |
| Commit 3e972b3ff8e532be233f70567c87512324c99b4e renamed coq.el, coq-db.el, coq-syntax.el to gallina.el, gallina-db.el, gallina-syntax.el without fixing up any of the references. Commit 30b58d43e48569afb50a35d3915ec7d453a61f5d only fixed up some of them. Here are some more (hopefully all of them). Signed-off-by: Anders Kaseorg <andersk@mit.edu> | |||
| 2014-10-03 | Fixing #3606 continued (doc of Scheme Boolean Equality Scheme). | Hugo Herbelin | |
| 2014-10-03 | Removing deactivated command Show Tree. | Hugo Herbelin | |
| 2014-09-29 | typo | Enrico Tassi | |
| 2014-09-29 | Documenting option -type-in-type. | Hugo Herbelin | |
| 2014-09-18 | seems to fix a looping coq-tex (when compiled with camlp4) | Pierre Boutillier | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |