aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-oth.tex
AgeCommit message (Expand)Author
2018-04-10[Sphinx] Move chapter 6 to new infrastructureMaxime Dénès
2018-02-28[toplevel] [vernac] Remove Load hack and check supported scenarios.Emilio Jesus Gallego Arias
2018-02-07mention interactive mode for Fail messagePaul Steckler
2018-01-25document the Fail commandPaul Steckler
2017-11-25Allow local universe renaming in Print.Gaëtan Gilbert
2017-09-22Avoid generated names for html pages of the reference manual (bug #4742).Guillaume Melquiond
2017-08-17Adding documentation for Printing Focused option.Pierre Courtieu
2017-07-27[toplevel] Remove long ago deprecated and NOOP options.Emilio Jesus Gallego Arias
2017-05-17Merge PR#457: Adding an even more compact goal hyps mode.Maxime Dénès
2017-05-11Documenting Printing Compact Contexts + CHANGESPierre Courtieu
2017-04-27fix order of command-line arguments mentioned in Add LoadPathPaul Steckler
2016-11-14Do not mention "none" in warnings doc, as it is there for compatibility.Maxime Dénès
2016-11-04Add documentation for [Set Warnings] and the -w option.Cyprien Mangin
2016-08-16Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-08-04Fix documentation typo (bug #4994).Guillaume Melquiond
2016-06-19Add [Unset Printing Dependent Evars Line]Jason Gross
2015-12-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-11Remove Set Virtual Machine from doc, since the command itself has been removed.Maxime Dénès
2015-10-06Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-04Fix typo. (Fix bug #4355)Guillaume Melquiond
2015-07-27search: Add an output-name-only search optionClément Pit--Claudel
2015-05-04Fix documentation of RedirectEnrico Tassi
2015-05-04Add a [Redirect] vernacular commandClément Pit--Claudel
2015-04-17Fixing a few typos + some uniformization of writing in doc.Hugo Herbelin
2015-04-15Documenting the recommandation of toplevel-only commands.Pierre-Marie Pédrot
2015-04-01Fixing a few typos + some uniformization of writing in doc.Hugo Herbelin
2015-04-01Documenting "From * Require *" and clearing a bit the loadpath chapter.Pierre-Marie Pédrot
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-02-17Remove Whelp commands.Maxime Dénès
2015-02-17Separate index for vernacular options.Maxime Dénès
2015-02-17Fix sentence that was cut in doc of Local Set.Maxime Dénès
2015-02-05Fix some documentation typos.Guillaume Melquiond
2015-01-29Remove spurious "Loading ML file" and "<W> Grammar extension" from the refere...Guillaume Melquiond
2014-12-25Document 6d5b56d971 (forbid Require inside modules).Maxime Dénès
2014-12-12Searchxxx now search also the hypothesis and support goal selector.Pierre Courtieu
2014-12-09refman: avoid label names with whitespace (unsupported in html)Pierre Letouzey
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-08-16Removing documentation related to the deprecated State machinery.Pierre-Marie Pédrot
2014-07-21Documenting the changes of Locate semantics.Pierre-Marie Pédrot
2014-06-21Fixing grammar in doc of Opaque as proposed by Jason (#3389).Hugo Herbelin
2014-03-20Documenting the Print Strategy command.Pierre-Marie Pédrot
2014-02-02Removing the [Require "file"] syntax.Pierre-Marie Pédrot
2014-01-13Fixing typo in reference manual from previous commitHugo Herbelin
2014-01-13Documenting old but useful command "Print Tables".Hugo Herbelin
2013-04-17Renaming SearchAbout into Search and Search into SearchHead.herbelin
2012-10-30Documenting the 'Printing Transparent/All Dependencies' command.ppedrot
2012-08-11Improving rendering of ldots in doc (partially done, there are tooherbelin
2012-08-03Document the command Add/Remove Search Blacklistletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:57:15 +0000