aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
* Start credits for 8.5.Gravatar Matthieu Sozeau2015-01-08
|
* Small fix in whodidwhat 8.5.Gravatar Pierre Courtieu2015-01-08
|
* Fixed and extend bullet related info/error messages. + doc.Gravatar Pierre Courtieu2015-01-08
| | | | | Had to put some hook in the handler of Proofview.NoSuchgoals. Documentation updated. CHANGE updated.
* Fix some documentation typos.Gravatar Guillaume Melquiond2015-01-08
|
* Add a few words in whodidwhat.Gravatar Maxime Dénès2015-01-08
|
* Document native_compute.Gravatar Maxime Dénès2015-01-08
|
* Initiating who-did-what for 8.5Gravatar Hugo Herbelin2015-01-07
|
* Committing whodidwhat files.Gravatar Hugo Herbelin2015-01-07
|
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
|
* Fix some documentation typos.Gravatar Guillaume Melquiond2015-01-06
|
* Added more informative messages about bullets.Gravatar Pierre Courtieu2015-01-05
| | | | Updated doc, but not tests-suite yet.
* Updating documentation about bullets.Gravatar Pierre Courtieu2015-01-05
| | | | Error messages were outdated.
* Document the new behavior of lazymatch.Gravatar Guillaume Melquiond2014-12-30
|
* Document 6d5b56d971 (forbid Require inside modules).Gravatar Maxime Dénès2014-12-25
|
* Better doc and a few fixes for Proof using.Gravatar Enrico Tassi2014-12-19
|
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
|
* Searchxxx now search also the hypothesis and support goal selector.Gravatar Pierre Courtieu2014-12-12
| | | | Documentation also updated.
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
|
* refman: switch all source files to utf8Gravatar Pierre Letouzey2014-12-09
| | | | | | 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.
* refman: fix broken urlsGravatar Pierre Letouzey2014-12-09
|
* refman: remove ?uri=referer in urls pointing to validator.w3.orgGravatar Pierre Letouzey2014-12-09
| | | | | | | | | | | 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.
* refman/Omega.tex: do not advertize Pierre Cregut's email for bug reportsGravatar Pierre Letouzey2014-12-09
|
* refman/coqdoc.tex: fix two erroneous \urlGravatar Pierre Letouzey2014-12-09
|
* refman: for xhtml validity, add 'alt' attributes to imgGravatar Pierre Letouzey2014-12-09
|
* refman: avoid label names with whitespace (unsupported in html)Gravatar Pierre Letouzey2014-12-09
|
* refman: xhtml validity of the cover pageGravatar Pierre Letouzey2014-12-09
|
* doc/stdlib: fix the xhtml validity of the index-list templateGravatar Pierre Letouzey2014-12-09
|
* doc: improved xhtml compatibility (cover, header,...)Gravatar Pierre Letouzey2014-12-09
|
* doc/stdlib: fix the html charset in header.html and coGravatar Pierre Letouzey2014-12-09
|
* doc: version number in cover.html + updates in coq.inria.fr styleGravatar Pierre Letouzey2014-12-09
| | | | To be continued someday, those style files are full of redundancies...
* Port to trunk commit r16062 of v8.4 (Correction des entêtes pour la ↵Gravatar notin2014-12-09
| | | | documentation en ligne)
* Port to trunk the old commit r14895 of v8.4 (styles for the stdlib ↵Gravatar notin2014-12-09
| | | | | | documentation) This commit r14895 comes apparently itself from commit r12010 in branch v8.2
* Documenting the Set Refine Instance Mode.Gravatar Pierre-Marie Pédrot2014-11-30
|
* FAQ: fix some broken urlsGravatar Pierre Letouzey2014-11-27
|
* typosGravatar Enrico Tassi2014-11-27
|
* Documenting the -color option.Gravatar Pierre-Marie Pédrot2014-11-17
|
* Documenting use of colors in Coq.Gravatar Pierre-Marie Pédrot2014-11-17
|
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | 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").
* Document (some) Proof using syntax + the new Optimize commandsGravatar Enrico Tassi2014-11-12
|
* Fixing doc of Functional Induction.Gravatar Hugo Herbelin2014-11-07
|
* doc: version number in cover.html + updates in coq.inria.fr styleGravatar Pierre Letouzey2014-11-07
|
* Documenting the change of semantics of the replace tactic.Gravatar Pierre-Marie Pédrot2014-11-04
|
* Document [Info] command.Gravatar Arnaud Spiwack2014-11-01
|
* Use the url package, since coqdoc generates \url commands.Gravatar Guillaume Melquiond2014-10-27
|
* Addressing report #3279 (inconsistency of behavior of the -> and <-Gravatar Hugo Herbelin2014-10-24
| | | | | | | | | | | | | | | 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.
* Fix typo in documentation of the [repeat] tactical.Gravatar Arnaud Spiwack2014-10-24
| | | Closes #3761.
* Move 'Arguments: clear implicits' to 2.7.4 (Close 2891)Gravatar Enrico Tassi2014-10-22
|
* More fallout from elisp renameGravatar Anders Kaseorg2014-10-16
| | | | | | | | | | 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>
* Fixing #3606 continued (doc of Scheme Boolean Equality Scheme).Gravatar Hugo Herbelin2014-10-03
|
* Removing deactivated command Show Tree.Gravatar Hugo Herbelin2014-10-03
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 05:57:18 +0000