aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
AgeCommit message (Expand)Author
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
2014-09-03Cbn in refmanPierre Boutillier
2014-09-02coqworkmgrEnrico Tassi
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-08-25Grammar: "allowing to" is not proper EnglishJason Gross
2014-08-18Adding a new intro-pattern for "apply in" on the fly. Using syntaxHugo Herbelin
2014-08-18Slight simplification of naming of tactics in equality.ml (hopefully).Hugo Herbelin
2014-08-16Removing documentation related to the deprecated State machinery.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 14:49:29 +0000