| Age | Commit message (Expand) | Author |
|---|
| 2014-12-09 | Port to trunk the old commit r14895 of v8.4 (styles for the stdlib documentat... | notin |
| 2014-11-30 | Documenting the Set Refine Instance Mode. | Pierre-Marie Pédrot |
| 2014-11-27 | FAQ: fix some broken urls | Pierre Letouzey |
| 2014-11-27 | typos | Enrico Tassi |
| 2014-11-17 | Documenting the -color option. | Pierre-Marie Pédrot |
| 2014-11-17 | Documenting use of colors in Coq. | Pierre-Marie Pédrot |
| 2014-11-16 | Enforcing a stronger difference between the two syntaxes "simpl | Hugo Herbelin |
| 2014-11-12 | Document (some) Proof using syntax + the new Optimize commands | Enrico Tassi |
| 2014-11-07 | Fixing doc of Functional Induction. | Hugo Herbelin |
| 2014-11-07 | doc: version number in cover.html + updates in coq.inria.fr style | Pierre Letouzey |
| 2014-11-04 | Documenting the change of semantics of the replace tactic. | Pierre-Marie Pédrot |
| 2014-11-01 | Document [Info] command. | Arnaud Spiwack |
| 2014-10-27 | Use the url package, since coqdoc generates \url commands. | Guillaume Melquiond |
| 2014-10-24 | Addressing report #3279 (inconsistency of behavior of the -> and <- | Hugo Herbelin |
| 2014-10-24 | Fix typo in documentation of the [repeat] tactical. | Arnaud Spiwack |
| 2014-10-22 | Move 'Arguments: clear implicits' to 2.7.4 (Close 2891) | Enrico Tassi |
| 2014-10-16 | More fallout from elisp rename | Anders Kaseorg |
| 2014-10-03 | Fixing #3606 continued (doc of Scheme Boolean Equality Scheme). | Hugo Herbelin |
| 2014-10-03 | Removing deactivated command Show Tree. | Hugo Herbelin |
| 2014-09-29 | typo | Enrico Tassi |
| 2014-09-29 | Documenting option -type-in-type. | Hugo Herbelin |
| 2014-09-18 | seems to fix a looping coq-tex (when compiled with camlp4) | Pierre Boutillier |
| 2014-09-11 | Fixing bug #3605. | Pierre-Marie Pédrot |
| 2014-09-11 | Removing remaining documentation of the XML plugin. | Pierre-Marie Pédrot |
| 2014-09-10 | Fixing inversion after having fixed intros_replacing | Hugo Herbelin |
| 2014-09-10 | Removing "eqn:" for "induction" in reference manual. | Hugo Herbelin |
| 2014-09-09 | Documenting the new Undo semantics | Enrico Tassi |
| 2014-09-08 | Removing the documentation of the XML plugin. | Pierre-Marie Pédrot |
| 2014-09-08 | Doc: [revgoals]. | Arnaud Spiwack |
| 2014-09-07 | Little fix in documentation of inversion. | Hugo Herbelin |
| 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 |
