| Age | Commit message (Expand) | Author |
|---|
| 2014-09-04 | Documenting the [Variant] type definition and the [Nonrecursive Elimination S... | Arnaud Spiwack |
| 2014-09-03 | sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.tex | Pierre Boutillier |
| 2014-09-03 | Improve RefMan section about Coq_makefile | Pierre Boutillier |
| 2014-09-03 | Update RefMan with respect to new loadpath management | Pierre Boutillier |
| 2014-09-03 | Cbn in refman | Pierre Boutillier |
| 2014-09-02 | coqworkmgr | Enrico Tassi |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 2014-08-25 | Grammar: "allowing to" is not proper English | Jason Gross |
| 2014-08-18 | Adding a new intro-pattern for "apply in" on the fly. Using syntax | Hugo Herbelin |
| 2014-08-18 | Slight simplification of naming of tactics in equality.ml (hopefully). | Hugo Herbelin |
| 2014-08-16 | Removing documentation related to the deprecated State machinery. | Pierre-Marie Pédrot |
| 2014-08-05 | Uncountably many bullets (+,-,*,++,--,**,+++,...). | Hugo Herbelin |
| 2014-08-05 | Experimentally adding an option for automatically erasing an | Hugo Herbelin |
| 2014-08-05 | Adding a syntax "enough" for the variant of "assert" with the order of | Hugo Herbelin |
| 2014-08-05 | Making references to Proof General and CoqIDE uniform in Reference Manual. | Hugo Herbelin |
| 2014-08-05 | Chapter 4 of reference manual: Fixing asymmetric patterns error + | Hugo Herbelin |
| 2014-08-05 | Documentation: a simple example for [numgoals]. | Arnaud Spiwack |
| 2014-08-05 | Documentation of [uconstr]: typesetting. | Arnaud Spiwack |
| 2014-08-05 | Documentation: refine accept uconstr arguments. | Arnaud Spiwack |
| 2014-08-05 | Doc: uconstr now has a tactic notation entry. | Arnaud Spiwack |
| 2014-08-03 | Chapter 4: Fixing ambiguity about whether the return predicate refers | Hugo Herbelin |
| 2014-08-01 | Document [> … ]. | Arnaud Spiwack |
| 2014-08-01 | Fix English spelling -> American spelling in doc. | Arnaud Spiwack |
| 2014-08-01 | Document [numgoals] and [guard]. | Arnaud Spiwack |
| 2014-07-31 | Typos. | Hugo Herbelin |
| 2014-07-29 | Document untyped terms in tactics. | Arnaud Spiwack |
| 2014-07-25 | Document swap tactic. | Arnaud Spiwack |
| 2014-07-25 | Document cycle tactic. | Arnaud Spiwack |
| 2014-07-25 | Update the documentation of Ltac's ";" and ";[…]" to reflect the new multi-... | Arnaud Spiwack |
| 2014-07-25 | Warns about inconsistency of generated name in evars and goals. | Arnaud Spiwack |
| 2014-07-25 | More documentation of universes. | Matthieu Sozeau |
| 2014-07-24 | Start documenting universe polymorphism. | Matthieu Sozeau |
| 2014-07-23 | Derive plugin: document new syntax. | Arnaud Spiwack |
| 2014-07-21 | Documenting the changes of Locate semantics. | Pierre-Marie Pédrot |
| 2014-07-15 | Added a (constructive) proof of Weak Konig's lemma for decidable trees. | Hugo Herbelin |
| 2014-07-13 | Adding a "time" tactical for benchmarking purposes. In case the tactic | Hugo Herbelin |
| 2014-07-09 | Arith: full integration of the "Numbers" modular framework | Pierre Letouzey |
| 2014-07-01 | Continuing ff9f94634 on making code and doc agree on "Set Equality Schemes" | Hugo Herbelin |
| 2014-06-26 | Avoid scanning .coq-native directories when building the library index. | Guillaume Melquiond |
| 2014-06-26 | Fix documentation. | Guillaume Melquiond |
| 2014-06-21 | Fixing grammar in doc of Opaque as proposed by Jason (#3389). | Hugo Herbelin |
| 2014-06-13 | Deprecate useless option -quality. | Guillaume Melquiond |
| 2014-06-13 | Remove documentation for the unsupported options -byte and -opt. | Guillaume Melquiond |
| 2014-06-13 | Deprecate options -dont, -lazy, -force-load-proofs. | Guillaume Melquiond |
| 2014-05-31 | More on injection over a projectable "existT". - Fixing syntax "injection ...... | Hugo Herbelin |
| 2014-05-08 | Typo reference manual | Hugo Herbelin |
| 2014-05-06 | - Fix index-list to show computational relations for rewriting files. | Matthieu Sozeau |
| 2014-04-28 | Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964) | Guillaume Melquiond |
| 2014-04-05 | Completing text of the question on conservativity of CIC over CC (bug #2697). | Hugo Herbelin |
| 2014-04-04 | Fix for bug #3107. | Guillaume Melquiond |
