aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2015-02-17Remove Whelp commands.Maxime Dénès
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.
2015-02-17Separate index for vernacular options.Maxime Dénès
2015-02-17Remove documentation of non-existing Show Implicits command.Maxime Dénès
2015-02-17Remove non-existing Tactic Definition command from index.Maxime Dénès
2015-02-17Fix sentence that was cut in doc of Local Set.Maxime Dénès
2015-02-16Documenting "induction t in ctx" when ctx contains an hyp not mentioning t.Hugo Herbelin
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
Of course such proofs cannot be processed asynchronously
2015-02-14dependent destruction: Fix (part of) bug #3961, by fixing dependent *Matthieu Sozeau
generalizing * which was broken since 8.4.
2015-02-12Fix typos about .vio files (thanks Arthur for spotting them)Enrico Tassi
2015-02-12Make clearer that "Remove Printing Let" does not influence destructuring let.Guillaume Melquiond
2015-02-10Avoid html markup inside tex files and fix url.Guillaume Melquiond
2015-02-10A few refinements in whodidwhat 8.4.Hugo Herbelin
2015-02-10Add section numbering to the refman PDF. (Fix for bug #2365)Guillaume Melquiond
2015-02-10Prevent Latex from messing with backticks. (Fix for bug #3871)Guillaume Melquiond
2015-02-10Fix documentation of generalize. (Fix for bug #4015)Guillaume Melquiond
2015-02-10Fix some documentation typo.Guillaume Melquiond
2015-02-05Fix some documentation typos.Guillaume Melquiond
2015-01-29Fix index of reference manual.Guillaume Melquiond
2015-01-29Remove spurious "Loading ML file" and "<W> Grammar extension" from the ↵Guillaume Melquiond
reference manual.
2015-01-29Remove some "Warning:" from the reference manual.Guillaume Melquiond
2015-01-29Fix some typos in the documentation.Guillaume Melquiond
2015-01-29Fix some broken Coq scripts in the reference manual.Guillaume Melquiond
2015-01-27Doc: Overfull lines in chapter on Canonical Structures.Hugo Herbelin
2015-01-24Doc: Fixing some compilation problems with chapter CanonicalHugo Herbelin
Structures. Text mode + a "Require Import" in a module which provokes suspect warnings "Exception Not_found".
2015-01-24Reference Manual: Documenting new printing of evars and new effect ofHugo Herbelin
Set Printing Existential Instances (see bug report #3951).
2015-01-21Reference Manual/Credits: expand the paragraph on the new proof engine to ↵Arnaud Spiwack
match the overall style.
2015-01-21Reference 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-21Reference manual/Credits: populate the "various smaller-scale improvements" ↵Arnaud Spiwack
part.
2015-01-21Reference Manual/Credits: remove a duplicate.Arnaud Spiwack
2015-01-21Reference manual: pass over the credit section for English.Arnaud Spiwack
2015-01-21Reference manual: fix typo in doc of [tryif/then/else].Arnaud Spiwack
Fixes #3939.
2015-01-17Univs: Complete documentation in refman.Matthieu Sozeau
2015-01-15Minor fixes to the refman credits to be continued.Matthieu Sozeau
2015-01-15Move explanations about primitive projections to the manual.Matthieu Sozeau
2015-01-15Expand Credits for 8.5 and doc on universesMatthieu Sozeau
2015-01-15Tentatively updating credits while remaining brief.Hugo Herbelin
2015-01-14Reference manual: I had previously omitted the syntax entry for [> t1|…|tn].Arnaud Spiwack
2015-01-14Reference manual: document tryif/then/else.Arnaud Spiwack
2015-01-14Reference manual: document multimatch.Arnaud Spiwack
2015-01-14Reference manual: try and improve documentation for Ltac's match.Arnaud Spiwack
In particular document the "once" behaviour.
2015-01-14Reference 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-14Reference manual: document gfail.Arnaud Spiwack
2015-01-13Refresh some copyright headers.Maxime Dénès
2015-01-13More documentation of the Local Definitions and Axioms.Pierre-Marie Pédrot
2015-01-12Whodidwhat-8.5: a global passArnaud Spiwack
Updating my own work and others when I could think of them.
2015-01-12whodidwhat-8.5: typo.Arnaud Spiwack
2015-01-11some credits for STMEnrico Tassi
2015-01-08Start credits for 8.5.Matthieu Sozeau
2015-01-08Small fix in whodidwhat 8.5.Pierre Courtieu
2015-01-08Fixed 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.