aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-ext.tex
Commit message (Expand)AuthorAge
* Update documentation of Arguments after recent changes.Gravatar Maxime Dénès2016-11-08
* Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.Gravatar Maxime Dénès2016-01-20
* Indexing and documenting some options.Gravatar Pierre-Marie Pédrot2015-12-12
* RefMan, ch. 4: Unify capitalization of "calculus of inductive constructions".Gravatar Hugo Herbelin2015-12-10
* RefMan, ch. 1 and 2: avoiding using the name "constant" whenGravatar Hugo Herbelin2015-12-06
* Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Gravatar Hugo Herbelin2015-12-02
* Adding the Printing Projections options to the index.Gravatar Pierre-Marie Pédrot2015-11-26
* Fix some broken Coq scripts in the documentation.Gravatar Guillaume Melquiond2015-07-30
* Remove obsolete documentation. (Fix bug #4238)Gravatar Guillaume Melquiond2015-07-22
* Fixing a few typos + some uniformization of writing in doc.Gravatar Hugo Herbelin2015-04-01
* More clarifications on loadpaths.Gravatar Pierre-Marie Pédrot2015-04-01
* Documenting "From * Require *" and clearing a bit the loadpath chapter.Gravatar Pierre-Marie Pédrot2015-04-01
* Separate index for vernacular options.Gravatar Maxime Dénès2015-02-17
* Fix typos about .vio files (thanks Arthur for spotting them)Gravatar Enrico Tassi2015-02-12
* Make clearer that "Remove Printing Let" does not influence destructuring let.Gravatar Guillaume Melquiond2015-02-12
* Prevent Latex from messing with backticks. (Fix for bug #3871)Gravatar Guillaume Melquiond2015-02-10
* Fix index of reference manual.Gravatar Guillaume Melquiond2015-01-29
* Remove some "Warning:" from the reference manual.Gravatar Guillaume Melquiond2015-01-29
* Reference Manual: Documenting new printing of evars and new effect ofGravatar Hugo Herbelin2015-01-24
* Move explanations about primitive projections to the manual.Gravatar Matthieu Sozeau2015-01-15
* refman: switch all source files to utf8Gravatar Pierre Letouzey2014-12-09
* Move 'Arguments: clear implicits' to 2.7.4 (Close 2891)Gravatar Enrico Tassi2014-10-22
* typoGravatar Enrico Tassi2014-09-29
* seems to fix a looping coq-tex (when compiled with camlp4)Gravatar Pierre Boutillier2014-09-18
* 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
* Update RefMan with respect to new loadpath managementGravatar Pierre Boutillier2014-09-03
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Documenting old but useful command "Print Tables".Gravatar Hugo Herbelin2014-01-13
* Documenting the tactic-in-term construction.Gravatar Pierre-Marie Pédrot2013-12-11
* Silence some warning about references in documentation.Gravatar Guillaume Melquiond2013-12-03
* First stab at documenting Canonical StructuresGravatar Enrico Tassi2013-11-29
* Manual fixed w.r.t. STMGravatar gareuselesinge2013-08-08
* Documentation of the "Local Definition" command.Gravatar ppedrot2013-03-11
* Added missing documentation of Set Printing Existential Instances.Gravatar herbelin2013-02-21
* Improving rendering of ...-separated lists and sequences in referenceGravatar herbelin2012-08-11
* Documentation of records defined with the keywords Inductive andGravatar aspiwack2012-04-13
* Added documentation for "Set Parsing Explicit" + fixed mistakenlyGravatar herbelin2012-01-20
* Fixed a Not_found bug when declaring in a section some implicitGravatar herbelin2011-12-18
* Command Arguments: standardizing format of error messages and American spelling.Gravatar herbelin2011-12-17
* Documentation of Arguments + implicitsGravatar gareuselesinge2011-12-06
* This adds two option tables 'Printing Record' and 'Printing Constructor'Gravatar herbelin2011-07-16
* This option disables the use of the '{| field := ... |}' notationGravatar herbelin2011-07-16
* @ in index of refman (last request of bug 2494)Gravatar pboutill2011-04-08
* Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)Gravatar herbelin2011-04-06
* Fix formatting issue in refmanGravatar glondu2011-01-12
* Add "Print Sorted Universes"Gravatar glondu2011-01-11
* Document DOT output of universe graphGravatar glondu2010-11-02
* Added multiple implicit arguments rules per name.Gravatar herbelin2010-10-03
* Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".Gravatar herbelin2010-06-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 13:53:19 +0000