aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2014-08-05Experimentally adding an option for automatically erasing anHugo Herbelin
2014-08-05Adding a syntax "enough" for the variant of "assert" with the order ofHugo Herbelin
2014-08-05Making references to Proof General and CoqIDE uniform in Reference Manual.Hugo Herbelin
2014-08-05Chapter 4 of reference manual: Fixing asymmetric patterns error +Hugo Herbelin
2014-08-05Documentation: a simple example for [numgoals].Arnaud Spiwack
2014-08-05Documentation of [uconstr]: typesetting.Arnaud Spiwack
2014-08-05Documentation: refine accept uconstr arguments.Arnaud Spiwack
2014-08-05Doc: uconstr now has a tactic notation entry.Arnaud Spiwack
2014-08-03Chapter 4: Fixing ambiguity about whether the return predicate refersHugo Herbelin
2014-08-01Document [> … ].Arnaud Spiwack
2014-08-01Fix English spelling -> American spelling in doc.Arnaud Spiwack
2014-08-01Document [numgoals] and [guard].Arnaud Spiwack
2014-07-31Typos.Hugo Herbelin
2014-07-29Document untyped terms in tactics.Arnaud Spiwack
2014-07-25Document swap tactic.Arnaud Spiwack
2014-07-25Document cycle tactic.Arnaud Spiwack
2014-07-25Update the documentation of Ltac's ";" and ";[…]" to reflect the new multi-...Arnaud Spiwack
2014-07-25Warns about inconsistency of generated name in evars and goals.Arnaud Spiwack
2014-07-25More documentation of universes.Matthieu Sozeau
2014-07-24Start documenting universe polymorphism.Matthieu Sozeau
2014-07-23Derive plugin: document new syntax.Arnaud Spiwack
2014-07-21Documenting the changes of Locate semantics.Pierre-Marie Pédrot
2014-07-15Added a (constructive) proof of Weak Konig's lemma for decidable trees.Hugo Herbelin
2014-07-13Adding a "time" tactical for benchmarking purposes. In case the tacticHugo Herbelin
2014-07-09Arith: full integration of the "Numbers" modular frameworkPierre Letouzey
2014-07-01Continuing ff9f94634 on making code and doc agree on "Set Equality Schemes"Hugo Herbelin
2014-06-26Avoid scanning .coq-native directories when building the library index.Guillaume Melquiond
2014-06-26Fix documentation.Guillaume Melquiond
2014-06-21Fixing grammar in doc of Opaque as proposed by Jason (#3389).Hugo Herbelin
2014-06-13Deprecate useless option -quality.Guillaume Melquiond
2014-06-13Remove documentation for the unsupported options -byte and -opt.Guillaume Melquiond
2014-06-13Deprecate options -dont, -lazy, -force-load-proofs.Guillaume Melquiond
2014-05-31More on injection over a projectable "existT". - Fixing syntax "injection ......Hugo Herbelin
2014-05-08Typo reference manualHugo Herbelin
2014-05-06- Fix index-list to show computational relations for rewriting files.Matthieu Sozeau
2014-04-28Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964)Guillaume Melquiond
2014-04-05Completing text of the question on conservativity of CIC over CC (bug #2697).Hugo Herbelin
2014-04-04Fix for bug #3107.Guillaume Melquiond
2014-04-04fixing Function docJulien Forest
2014-04-02Fix Bug 3131 + Really drop mentions of info in refman.Pierre Boutillier
2014-03-20Documenting the Print Strategy command.Pierre-Marie Pédrot
2014-02-26refman: document vi2voEnrico Tassi
2014-02-24fixup complement FinPierre Boutillier
2014-02-02Removing the [Require "file"] syntax.Pierre-Marie Pédrot
2014-01-26-schedule-vi-checking ported to spawnEnrico Tassi
2014-01-13Fixing typo in reference manual from previous commitHugo Herbelin
2014-01-13Documenting old but useful command "Print Tables".Hugo Herbelin
2014-01-05refman: fist stab at Asynchronous ProofsEnrico Tassi
2014-01-01Reference the 'external' tactic.Guillaume Melquiond
2013-12-20micromega: removal of spurious Export; addition of Lia.v encapsulating lia an...Frédéric Besson
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 03:13:02 +0000