aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
Commit message (Expand)AuthorAge
* Start credits for 8.5.Gravatar Matthieu Sozeau2015-01-08
* Fixed and extend bullet related info/error messages. + doc.Gravatar Pierre Courtieu2015-01-08
* Fix some documentation typos.Gravatar Guillaume Melquiond2015-01-08
* Document native_compute.Gravatar Maxime Dénès2015-01-08
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
* Fix some documentation typos.Gravatar Guillaume Melquiond2015-01-06
* Added more informative messages about bullets.Gravatar Pierre Courtieu2015-01-05
* Updating documentation about bullets.Gravatar Pierre Courtieu2015-01-05
* Document the new behavior of lazymatch.Gravatar Guillaume Melquiond2014-12-30
* Document 6d5b56d971 (forbid Require inside modules).Gravatar Maxime Dénès2014-12-25
* Better doc and a few fixes for Proof using.Gravatar Enrico Tassi2014-12-19
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
* Searchxxx now search also the hypothesis and support goal selector.Gravatar Pierre Courtieu2014-12-12
* refman: switch all source files to utf8Gravatar Pierre Letouzey2014-12-09
* refman: fix broken urlsGravatar Pierre Letouzey2014-12-09
* refman/Omega.tex: do not advertize Pierre Cregut's email for bug reportsGravatar Pierre Letouzey2014-12-09
* refman/coqdoc.tex: fix two erroneous \urlGravatar Pierre Letouzey2014-12-09
* refman: for xhtml validity, add 'alt' attributes to imgGravatar Pierre Letouzey2014-12-09
* refman: avoid label names with whitespace (unsupported in html)Gravatar Pierre Letouzey2014-12-09
* Documenting the Set Refine Instance Mode.Gravatar Pierre-Marie Pédrot2014-11-30
* 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
* Documenting the change of semantics of the replace tactic.Gravatar Pierre-Marie Pédrot2014-11-04
* Document [Info] command.Gravatar Arnaud Spiwack2014-11-01
* 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