aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
AgeCommit message (Expand)Author
2015-01-11some credits for STMEnrico Tassi
2015-01-08Start credits for 8.5.Matthieu Sozeau
2015-01-08Fixed and extend bullet related info/error messages. + doc.Pierre Courtieu
2015-01-08Fix some documentation typos.Guillaume Melquiond
2015-01-08Document native_compute.Maxime Dénès
2015-01-06rename: vi -> vioEnrico Tassi
2015-01-06Fix some documentation typos.Guillaume Melquiond
2015-01-05Added more informative messages about bullets.Pierre Courtieu
2015-01-05Updating documentation about bullets.Pierre Courtieu
2014-12-30Document the new behavior of lazymatch.Guillaume Melquiond
2014-12-25Document 6d5b56d971 (forbid Require inside modules).Maxime Dénès
2014-12-19Better doc and a few fixes for Proof using.Enrico Tassi
2014-12-18Proof using: New vernacular to name sets of section variablesEnrico Tassi
2014-12-12Searchxxx now search also the hypothesis and support goal selector.Pierre Courtieu
2014-12-09refman: switch all source files to utf8Pierre Letouzey
2014-12-09refman: fix broken urlsPierre Letouzey
2014-12-09refman/Omega.tex: do not advertize Pierre Cregut's email for bug reportsPierre Letouzey
2014-12-09refman/coqdoc.tex: fix two erroneous \urlPierre Letouzey
2014-12-09refman: for xhtml validity, add 'alt' attributes to imgPierre Letouzey
2014-12-09refman: avoid label names with whitespace (unsupported in html)Pierre Letouzey
2014-11-30Documenting the Set Refine Instance Mode.Pierre-Marie Pédrot
2014-11-27typosEnrico Tassi
2014-11-17Documenting the -color option.Pierre-Marie Pédrot
2014-11-17Documenting use of colors in Coq.Pierre-Marie Pédrot
2014-11-16Enforcing a stronger difference between the two syntaxes "simplHugo Herbelin
2014-11-12Document (some) Proof using syntax + the new Optimize commandsEnrico Tassi
2014-11-07Fixing doc of Functional Induction.Hugo Herbelin
2014-11-04Documenting the change of semantics of the replace tactic.Pierre-Marie Pédrot
2014-11-01Document [Info] command.Arnaud Spiwack
2014-10-24Addressing report #3279 (inconsistency of behavior of the -> and <-Hugo Herbelin
2014-10-24Fix typo in documentation of the [repeat] tactical.Arnaud Spiwack
2014-10-22Move 'Arguments: clear implicits' to 2.7.4 (Close 2891)Enrico Tassi
2014-10-16More fallout from elisp renameAnders Kaseorg
2014-10-03Fixing #3606 continued (doc of Scheme Boolean Equality Scheme).Hugo Herbelin
2014-10-03Removing deactivated command Show Tree.Hugo Herbelin
2014-09-29typoEnrico Tassi
2014-09-29Documenting option -type-in-type.Hugo Herbelin
2014-09-18seems to fix a looping coq-tex (when compiled with camlp4)Pierre Boutillier
2014-09-11Fixing bug #3605.Pierre-Marie Pédrot
2014-09-11Removing remaining documentation of the XML plugin.Pierre-Marie Pédrot
2014-09-10Fixing inversion after having fixed intros_replacingHugo Herbelin
2014-09-10Removing "eqn:" for "induction" in reference manual.Hugo Herbelin
2014-09-09Documenting the new Undo semanticsEnrico Tassi
2014-09-08Removing the documentation of the XML plugin.Pierre-Marie Pédrot
2014-09-08Doc: [revgoals].Arnaud Spiwack
2014-09-07Little fix in documentation of inversion.Hugo Herbelin
2014-09-04Documenting the [Variant] type definition and the [Nonrecursive Elimination S...Arnaud Spiwack
2014-09-03sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.texPierre Boutillier
2014-09-03Improve RefMan section about Coq_makefilePierre Boutillier
2014-09-03Update RefMan with respect to new loadpath managementPierre Boutillier
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 15:09:30 +0000