aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-oth.tex
Commit message (Expand)AuthorAge
* [Sphinx] Move chapter 6 to new infrastructureGravatar Maxime Dénès2018-04-10
* [toplevel] [vernac] Remove Load hack and check supported scenarios.Gravatar Emilio Jesus Gallego Arias2018-02-28
* mention interactive mode for Fail messageGravatar Paul Steckler2018-02-07
* document the Fail commandGravatar Paul Steckler2018-01-25
* Allow local universe renaming in Print.Gravatar Gaëtan Gilbert2017-11-25
* Avoid generated names for html pages of the reference manual (bug #4742).Gravatar Guillaume Melquiond2017-09-22
* Adding documentation for Printing Focused option.Gravatar Pierre Courtieu2017-08-17
* [toplevel] Remove long ago deprecated and NOOP options.Gravatar Emilio Jesus Gallego Arias2017-07-27
* Merge PR#457: Adding an even more compact goal hyps mode.Gravatar Maxime Dénès2017-05-17
|\
| * Documenting Printing Compact Contexts + CHANGESGravatar Pierre Courtieu2017-05-11
* | fix order of command-line arguments mentioned in Add LoadPathGravatar Paul Steckler2017-04-27
|/
* Do not mention "none" in warnings doc, as it is there for compatibility.Gravatar Maxime Dénès2016-11-14
* Add documentation for [Set Warnings] and the -w option.Gravatar Cyprien Mangin2016-11-04
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\
| * Fix documentation typo (bug #4994).Gravatar Guillaume Melquiond2016-08-04
* | Add [Unset Printing Dependent Evars Line]Gravatar Jason Gross2016-06-19
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-11
|\|
| * Remove Set Virtual Machine from doc, since the command itself has been removed.Gravatar Maxime Dénès2015-12-11
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-06
|\|
| * Fix typo. (Fix bug #4355)Gravatar Guillaume Melquiond2015-10-04
* | search: Add an output-name-only search optionGravatar Clément Pit--Claudel2015-07-27
|/
* Fix documentation of RedirectGravatar Enrico Tassi2015-05-04
* Add a [Redirect] vernacular commandGravatar Clément Pit--Claudel2015-05-04
* Fixing a few typos + some uniformization of writing in doc.Gravatar Hugo Herbelin2015-04-17
* Documenting the recommandation of toplevel-only commands.Gravatar Pierre-Marie Pédrot2015-04-15
* Fixing a few typos + some uniformization of writing in doc.Gravatar Hugo Herbelin2015-04-01
* Documenting "From * Require *" and clearing a bit the loadpath chapter.Gravatar Pierre-Marie Pédrot2015-04-01
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Remove Whelp commands.Gravatar Maxime Dénès2015-02-17
* Separate index for vernacular options.Gravatar Maxime Dénès2015-02-17
* Fix sentence that was cut in doc of Local Set.Gravatar Maxime Dénès2015-02-17
* Fix some documentation typos.Gravatar Guillaume Melquiond2015-02-05
* Remove spurious "Loading ML file" and "<W> Grammar extension" from the refere...Gravatar Guillaume Melquiond2015-01-29
* Document 6d5b56d971 (forbid Require inside modules).Gravatar Maxime Dénès2014-12-25
* Searchxxx now search also the hypothesis and support goal selector.Gravatar Pierre Courtieu2014-12-12
* refman: avoid label names with whitespace (unsupported in html)Gravatar Pierre Letouzey2014-12-09
* 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
* Removing documentation related to the deprecated State machinery.Gravatar Pierre-Marie Pédrot2014-08-16
* Documenting the changes of Locate semantics.Gravatar Pierre-Marie Pédrot2014-07-21
* Fixing grammar in doc of Opaque as proposed by Jason (#3389).Gravatar Hugo Herbelin2014-06-21
* Documenting the Print Strategy command.Gravatar Pierre-Marie Pédrot2014-03-20
* Removing the [Require "file"] syntax.Gravatar Pierre-Marie Pédrot2014-02-02
* Fixing typo in reference manual from previous commitGravatar Hugo Herbelin2014-01-13
* Documenting old but useful command "Print Tables".Gravatar Hugo Herbelin2014-01-13
* Renaming SearchAbout into Search and Search into SearchHead.Gravatar herbelin2013-04-17
* Documenting the 'Printing Transparent/All Dependencies' command.Gravatar ppedrot2012-10-30
* Improving rendering of ldots in doc (partially done, there are tooGravatar herbelin2012-08-11
* Document the command Add/Remove Search BlacklistGravatar letouzey2012-08-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 05:04:17 +0000