aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
...
* Fixing bug 3099.Gravatar Pierre-Marie Pédrot2015-02-26
|
* Fixed doc of fresh (was already outdated before fixing #3233).Gravatar Pierre Courtieu2015-02-23
|
* Remove Whelp commands.Gravatar Maxime Dénès2015-02-17
| | | | | | Although these commands were never deprecated, they have been unusable for some time now, since they send requests to an Italian server which is no longer alive.
* Separate index for vernacular options.Gravatar Maxime Dénès2015-02-17
|
* Remove documentation of non-existing Show Implicits command.Gravatar Maxime Dénès2015-02-17
|
* Remove non-existing Tactic Definition command from index.Gravatar Maxime Dénès2015-02-17
|
* Fix sentence that was cut in doc of Local Set.Gravatar Maxime Dénès2015-02-17
|
* Documenting "induction t in ctx" when ctx contains an hyp not mentioning t.Gravatar Hugo Herbelin2015-02-16
|
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
| | | | Of course such proofs cannot be processed asynchronously
* dependent destruction: Fix (part of) bug #3961, by fixing dependent *Gravatar Matthieu Sozeau2015-02-14
| | | | generalizing * which was broken since 8.4.
* Fix typos about .vio files (thanks Arthur for spotting them)Gravatar Enrico Tassi2015-02-12
|
* Make clearer that "Remove Printing Let" does not influence destructuring let.Gravatar Guillaume Melquiond2015-02-12
|
* Avoid html markup inside tex files and fix url.Gravatar Guillaume Melquiond2015-02-10
|
* A few refinements in whodidwhat 8.4.Gravatar Hugo Herbelin2015-02-10
|
* Add section numbering to the refman PDF. (Fix for bug #2365)Gravatar Guillaume Melquiond2015-02-10
|
* Prevent Latex from messing with backticks. (Fix for bug #3871)Gravatar Guillaume Melquiond2015-02-10
|
* Fix documentation of generalize. (Fix for bug #4015)Gravatar Guillaume Melquiond2015-02-10
|
* Fix some documentation typo.Gravatar Guillaume Melquiond2015-02-10
|
* Fix some documentation typos.Gravatar Guillaume Melquiond2015-02-05
|
* Fix index of reference manual.Gravatar Guillaume Melquiond2015-01-29
|
* Remove spurious "Loading ML file" and "<W> Grammar extension" from the ↵Gravatar Guillaume Melquiond2015-01-29
| | | | reference manual.
* Remove some "Warning:" from the reference manual.Gravatar Guillaume Melquiond2015-01-29
|
* Fix some typos in the documentation.Gravatar Guillaume Melquiond2015-01-29
|
* Fix some broken Coq scripts in the reference manual.Gravatar Guillaume Melquiond2015-01-29
|
* Doc: Overfull lines in chapter on Canonical Structures.Gravatar Hugo Herbelin2015-01-27
|
* Doc: Fixing some compilation problems with chapter CanonicalGravatar Hugo Herbelin2015-01-24
| | | | | Structures. Text mode + a "Require Import" in a module which provokes suspect warnings "Exception Not_found".
* Reference Manual: Documenting new printing of evars and new effect ofGravatar Hugo Herbelin2015-01-24
| | | | Set Printing Existential Instances (see bug report #3951).
* Reference Manual/Credits: expand the paragraph on the new proof engine to ↵Gravatar Arnaud Spiwack2015-01-21
| | | | match the overall style.
* Reference Manual/Credits: native compute is a major contribution.Gravatar Arnaud Spiwack2015-01-21
| | | 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.
* Reference manual/Credits: populate the "various smaller-scale improvements" ↵Gravatar Arnaud Spiwack2015-01-21
| | | | part.
* Reference Manual/Credits: remove a duplicate.Gravatar Arnaud Spiwack2015-01-21
|
* Reference manual: pass over the credit section for English.Gravatar Arnaud Spiwack2015-01-21
|
* Reference manual: fix typo in doc of [tryif/then/else].Gravatar Arnaud Spiwack2015-01-21
| | | Fixes #3939.
* Univs: Complete documentation in refman.Gravatar Matthieu Sozeau2015-01-17
|
* Minor fixes to the refman credits to be continued.Gravatar Matthieu Sozeau2015-01-15
|
* Move explanations about primitive projections to the manual.Gravatar Matthieu Sozeau2015-01-15
|
* Expand Credits for 8.5 and doc on universesGravatar Matthieu Sozeau2015-01-15
|
* Tentatively updating credits while remaining brief.Gravatar Hugo Herbelin2015-01-15
|
* Reference manual: I had previously omitted the syntax entry for [> t1|…|tn].Gravatar Arnaud Spiwack2015-01-14
|
* Reference manual: document tryif/then/else.Gravatar Arnaud Spiwack2015-01-14
|
* Reference manual: document multimatch.Gravatar Arnaud Spiwack2015-01-14
|
* Reference manual: try and improve documentation for Ltac's match.Gravatar Arnaud Spiwack2015-01-14
| | | | In particular document the "once" behaviour.
* Reference manual: try and improve the documentation of lazymatch.Gravatar Arnaud Spiwack2015-01-14
| | | | In particular try to avoid the use of the word "backtracking" which refers to too many things.
* Reference manual: document gfail.Gravatar Arnaud Spiwack2015-01-14
|
* Refresh some copyright headers.Gravatar Maxime Dénès2015-01-13
|
* More documentation of the Local Definitions and Axioms.Gravatar Pierre-Marie Pédrot2015-01-13
|
* Whodidwhat-8.5: a global passGravatar Arnaud Spiwack2015-01-12
| | | Updating my own work and others when I could think of them.
* whodidwhat-8.5: typo.Gravatar Arnaud Spiwack2015-01-12
|
* some credits for STMGravatar Enrico Tassi2015-01-11
|
* Start credits for 8.5.Gravatar Matthieu Sozeau2015-01-08
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 03:13:58 +0000