aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-ext.tex
AgeCommit message (Expand)Author
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
2017-04-12Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...Maxime Dénès
2017-04-09Merge PR#460: Turning the printing primitive projection compatibility flag of...Maxime Dénès
2017-04-07Merge PR#485: Document Show MatchMaxime Dénès
2017-04-07Turning the printing primitive projection parameter flag off by default.Hugo Herbelin
2017-04-07Turning the printing primitive projection compatibility flag off by default.Hugo Herbelin
2017-03-23Documenting the grammar {| ... |} syntax for building records.Hugo Herbelin
2017-03-17Document Show Match, add ref to that in match variants/extensionsPaul Steckler
2017-03-14[toplevel] Remove unusable option -notopEmilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 14:19:31 +0000