aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Fix various typos in documentationGravatar Matěj Grabovský2015-03-31
* Qed export -> Qed exportingGravatar Enrico Tassi2015-03-22
* Index MMaps files, otherwise documentation cannot be built. (Fix for bug #4107)Gravatar Guillaume Melquiond2015-03-21
* Fixing #4127 (command for locating exists notation in refman changed).Gravatar Hugo Herbelin2015-03-13
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Preprend Fail to all the expected failures in the documentation.Gravatar Guillaume Melquiond2015-03-05
* Typos in doc modules.Gravatar Hugo Herbelin2015-03-03
* 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
* 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
* dependent destruction: Fix (part of) bug #3961, by fixing dependent *Gravatar Matthieu Sozeau2015-02-14
* 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 refere...Gravatar Guillaume Melquiond2015-01-29
* 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
* Reference Manual: Documenting new printing of evars and new effect ofGravatar Hugo Herbelin2015-01-24
* Reference Manual/Credits: expand the paragraph on the new proof engine to mat...Gravatar Arnaud Spiwack2015-01-21
* Reference Manual/Credits: native compute is a major contribution.Gravatar Arnaud Spiwack2015-01-21
* Reference manual/Credits: populate the "various smaller-scale improvements" p...Gravatar Arnaud Spiwack2015-01-21
* 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
* 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
* Reference manual: try and improve the documentation of lazymatch.Gravatar Arnaud Spiwack2015-01-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 22:15:26 +0000