| Commit message (Expand) | Author | Age |
* | Documenting the Set Refine Instance Mode. | Pierre-Marie Pédrot | 2014-11-30 |
* | FAQ: fix some broken urls | Pierre Letouzey | 2014-11-27 |
* | typos | Enrico Tassi | 2014-11-27 |
* | Documenting the -color option. | Pierre-Marie Pédrot | 2014-11-17 |
* | Documenting use of colors in Coq. | Pierre-Marie Pédrot | 2014-11-17 |
* | Enforcing a stronger difference between the two syntaxes "simpl | Hugo Herbelin | 2014-11-16 |
* | Document (some) Proof using syntax + the new Optimize commands | Enrico Tassi | 2014-11-12 |
* | 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-07 |
* | Documenting the change of semantics of the replace tactic. | Pierre-Marie Pédrot | 2014-11-04 |
* | Document [Info] command. | Arnaud Spiwack | 2014-11-01 |
* | Use the url package, since coqdoc generates \url commands. | Guillaume Melquiond | 2014-10-27 |
* | 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-24 |
* | Move 'Arguments: clear implicits' to 2.7.4 (Close 2891) | Enrico Tassi | 2014-10-22 |
* | More fallout from elisp rename | Anders Kaseorg | 2014-10-16 |
* | Fixing #3606 continued (doc of Scheme Boolean Equality Scheme). | Hugo Herbelin | 2014-10-03 |
* | Removing deactivated command Show Tree. | Hugo Herbelin | 2014-10-03 |
* | typo | Enrico Tassi | 2014-09-29 |
* | Documenting option -type-in-type. | Hugo Herbelin | 2014-09-29 |
* | seems to fix a looping coq-tex (when compiled with camlp4) | Pierre Boutillier | 2014-09-18 |
* | Fixing bug #3605. | Pierre-Marie Pédrot | 2014-09-11 |
* | Removing remaining documentation of the XML plugin. | Pierre-Marie Pédrot | 2014-09-11 |
* | Fixing inversion after having fixed intros_replacing | Hugo Herbelin | 2014-09-10 |
* | Removing "eqn:" for "induction" in reference manual. | Hugo Herbelin | 2014-09-10 |
* | Documenting the new Undo semantics | Enrico Tassi | 2014-09-09 |
* | Removing the documentation of the XML plugin. | Pierre-Marie Pédrot | 2014-09-08 |
* | Doc: [revgoals]. | Arnaud Spiwack | 2014-09-08 |
* | Little fix in documentation of inversion. | Hugo Herbelin | 2014-09-07 |
* | Documenting the [Variant] type definition and the [Nonrecursive Elimination S... | Arnaud Spiwack | 2014-09-04 |
* | 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-03 |
* | coqworkmgr | Enrico Tassi | 2014-09-02 |
* | "allows to", like "allowing to", is improper | Jason Gross | 2014-08-25 |
* | Grammar: "allowing to" is not proper English | Jason Gross | 2014-08-25 |
* | 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-18 |
* | Removing documentation related to the deprecated State machinery. | Pierre-Marie Pédrot | 2014-08-16 |
* | 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-05 |
* | Chapter 4: Fixing ambiguity about whether the return predicate refers | Hugo Herbelin | 2014-08-03 |