aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2015-02-17Remove Whelp commands.Maxime Dénès
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
2015-02-14dependent destruction: Fix (part of) bug #3961, by fixing dependent *Matthieu Sozeau
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 refere...Guillaume Melquiond
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
2015-01-24Reference Manual: Documenting new printing of evars and new effect ofHugo Herbelin
2015-01-21Reference Manual/Credits: expand the paragraph on the new proof engine to mat...Arnaud Spiwack
2015-01-21Reference Manual/Credits: native compute is a major contribution.Arnaud Spiwack
2015-01-21Reference manual/Credits: populate the "various smaller-scale improvements" p...Arnaud Spiwack
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
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
2015-01-14Reference manual: try and improve the documentation of lazymatch.Arnaud Spiwack
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 21:05:03 +0000