aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* 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
* 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
* 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
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 08:53:20 +0000