aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Documenting the Set Refine Instance Mode.Gravatar Pierre-Marie Pédrot2014-11-30
* FAQ: fix some broken urlsGravatar Pierre Letouzey2014-11-27
* typosGravatar Enrico Tassi2014-11-27
* Documenting the -color option.Gravatar Pierre-Marie Pédrot2014-11-17
* Documenting use of colors in Coq.Gravatar Pierre-Marie Pédrot2014-11-17
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Document (some) Proof using syntax + the new Optimize commandsGravatar Enrico Tassi2014-11-12
* Fixing doc of Functional Induction.Gravatar Hugo Herbelin2014-11-07
* doc: version number in cover.html + updates in coq.inria.fr styleGravatar Pierre Letouzey2014-11-07
* Documenting the change of semantics of the replace tactic.Gravatar Pierre-Marie Pédrot2014-11-04
* Document [Info] command.Gravatar Arnaud Spiwack2014-11-01
* Use the url package, since coqdoc generates \url commands.Gravatar Guillaume Melquiond2014-10-27
* Addressing report #3279 (inconsistency of behavior of the -> and <-Gravatar Hugo Herbelin2014-10-24
* Fix typo in documentation of the [repeat] tactical.Gravatar Arnaud Spiwack2014-10-24
* Move 'Arguments: clear implicits' to 2.7.4 (Close 2891)Gravatar Enrico Tassi2014-10-22
* More fallout from elisp renameGravatar Anders Kaseorg2014-10-16
* Fixing #3606 continued (doc of Scheme Boolean Equality Scheme).Gravatar Hugo Herbelin2014-10-03
* Removing deactivated command Show Tree.Gravatar Hugo Herbelin2014-10-03
* typoGravatar Enrico Tassi2014-09-29
* Documenting option -type-in-type.Gravatar Hugo Herbelin2014-09-29
* seems to fix a looping coq-tex (when compiled with camlp4)Gravatar Pierre Boutillier2014-09-18
* Fixing bug #3605.Gravatar Pierre-Marie Pédrot2014-09-11
* Removing remaining documentation of the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-11
* Fixing inversion after having fixed intros_replacingGravatar Hugo Herbelin2014-09-10
* Removing "eqn:" for "induction" in reference manual.Gravatar Hugo Herbelin2014-09-10
* Documenting the new Undo semanticsGravatar Enrico Tassi2014-09-09
* Removing the documentation of the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Doc: [revgoals].Gravatar Arnaud Spiwack2014-09-08
* Little fix in documentation of inversion.Gravatar Hugo Herbelin2014-09-07
* Documenting the [Variant] type definition and the [Nonrecursive Elimination S...Gravatar Arnaud Spiwack2014-09-04
* sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.texGravatar Pierre Boutillier2014-09-03
* Improve RefMan section about Coq_makefileGravatar Pierre Boutillier2014-09-03
* Update RefMan with respect to new loadpath managementGravatar Pierre Boutillier2014-09-03
* Cbn in refmanGravatar Pierre Boutillier2014-09-03
* coqworkmgrGravatar Enrico Tassi2014-09-02
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Grammar: "allowing to" is not proper EnglishGravatar Jason Gross2014-08-25
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
* Slight simplification of naming of tactics in equality.ml (hopefully).Gravatar Hugo Herbelin2014-08-18
* Removing documentation related to the deprecated State machinery.Gravatar Pierre-Marie Pédrot2014-08-16
* Uncountably many bullets (+,-,*,++,--,**,+++,...).Gravatar Hugo Herbelin2014-08-05
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
* Adding a syntax "enough" for the variant of "assert" with the order ofGravatar Hugo Herbelin2014-08-05
* Making references to Proof General and CoqIDE uniform in Reference Manual.Gravatar Hugo Herbelin2014-08-05
* Chapter 4 of reference manual: Fixing asymmetric patterns error +Gravatar Hugo Herbelin2014-08-05
* Documentation: a simple example for [numgoals].Gravatar Arnaud Spiwack2014-08-05
* Documentation of [uconstr]: typesetting.Gravatar Arnaud Spiwack2014-08-05
* Documentation: refine accept uconstr arguments.Gravatar Arnaud Spiwack2014-08-05
* Doc: uconstr now has a tactic notation entry.Gravatar Arnaud Spiwack2014-08-05
* Chapter 4: Fixing ambiguity about whether the return predicate refersGravatar Hugo Herbelin2014-08-03