aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-ext.tex
AgeCommit message (Expand)Author
2016-11-08Update documentation of Arguments after recent changes.Maxime Dénès
2016-01-20Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.Maxime Dénès
2015-12-12Indexing and documenting some options.Pierre-Marie Pédrot
2015-12-10RefMan, ch. 4: Unify capitalization of "calculus of inductive constructions".Hugo Herbelin
2015-12-06RefMan, ch. 1 and 2: avoiding using the name "constant" whenHugo Herbelin
2015-12-02Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Hugo Herbelin
2015-11-26Adding the Printing Projections options to the index.Pierre-Marie Pédrot
2015-07-30Fix some broken Coq scripts in the documentation.Guillaume Melquiond
2015-07-22Remove obsolete documentation. (Fix bug #4238)Guillaume Melquiond
2015-04-01Fixing a few typos + some uniformization of writing in doc.Hugo Herbelin
2015-04-01More clarifications on loadpaths.Pierre-Marie Pédrot
2015-04-01Documenting "From * Require *" and clearing a bit the loadpath chapter.Pierre-Marie Pédrot
2015-02-17Separate index for vernacular options.Maxime Dénès
2015-02-12Fix typos about .vio files (thanks Arthur for spotting them)Enrico Tassi
2015-02-12Make clearer that "Remove Printing Let" does not influence destructuring let.Guillaume Melquiond
2015-02-10Prevent Latex from messing with backticks. (Fix for bug #3871)Guillaume Melquiond
2015-01-29Fix index of reference manual.Guillaume Melquiond
2015-01-29Remove some "Warning:" from the reference manual.Guillaume Melquiond
2015-01-24Reference Manual: Documenting new printing of evars and new effect ofHugo Herbelin
2015-01-15Move explanations about primitive projections to the manual.Matthieu Sozeau
2014-12-09refman: switch all source files to utf8Pierre Letouzey
2014-10-22Move 'Arguments: clear implicits' to 2.7.4 (Close 2891)Enrico Tassi
2014-09-29typoEnrico Tassi
2014-09-18seems to fix a looping coq-tex (when compiled with camlp4)Pierre Boutillier
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-03Update RefMan with respect to new loadpath managementPierre Boutillier
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-01-13Documenting old but useful command "Print Tables".Hugo Herbelin
2013-12-11Documenting the tactic-in-term construction.Pierre-Marie Pédrot
2013-12-03Silence some warning about references in documentation.Guillaume Melquiond
2013-11-29First stab at documenting Canonical StructuresEnrico Tassi
2013-08-08Manual fixed w.r.t. STMgareuselesinge
2013-03-11Documentation of the "Local Definition" command.ppedrot
2013-02-21Added missing documentation of Set Printing Existential Instances.herbelin
2012-08-11Improving rendering of ...-separated lists and sequences in referenceherbelin
2012-04-13Documentation of records defined with the keywords Inductive andaspiwack
2012-01-20Added documentation for "Set Parsing Explicit" + fixed mistakenlyherbelin
2011-12-18Fixed a Not_found bug when declaring in a section some implicitherbelin
2011-12-17Command Arguments: standardizing format of error messages and American spelling.herbelin
2011-12-06Documentation of Arguments + implicitsgareuselesinge
2011-07-16This adds two option tables 'Printing Record' and 'Printing Constructor'herbelin
2011-07-16This option disables the use of the '{| field := ... |}' notationherbelin
2011-04-08@ in index of refman (last request of bug 2494)pboutill
2011-04-06Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)herbelin
2011-01-12Fix formatting issue in refmanglondu
2011-01-11Add "Print Sorted Universes"glondu
2010-11-02Document DOT output of universe graphglondu
2010-10-03Added multiple implicit arguments rules per name.herbelin
2010-06-08Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 17:22:34 +0000