aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-oth.tex
AgeCommit message (Collapse)Author
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
Minor clean up, no sense in having these as they do nothing.
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
This allows a work-around for bug #4819, https://coq.inria.fr/bugs/show_bug.cgi?id=4819.
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
When set, search results only display symbol names, instead of displaying full terms with types. This is useful when the list of symbols is needed by an external program, in particular for doing completion in IDEs.
2015-05-04Fix documentation of RedirectEnrico Tassi
2015-05-04Add a [Redirect] vernacular commandClément Pit--Claudel
The command [Redirect "filename" (...)] redirects all the output of [(...)] to file "filename.out". This is useful for storing the results of an [Eval compute], for redirecting the results of a large search, for automatically generating traces of interesting developments, and so on.
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
- no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit
2015-02-17Remove Whelp commands.Maxime Dénès
Although these commands were never deprecated, they have been unusable for some time now, since they send requests to an Italian server which is no longer alive.
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 ↵Guillaume Melquiond
reference manual.
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
Documentation also updated.
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
It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar).
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
Made a synonymous of it ("Print Options"). Also reorganized a bit the section about flags and options in reference manual.
2013-04-17Renaming SearchAbout into Search and Search into SearchHead.herbelin
I hope I did not forget any place to change. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16423 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-30Documenting the 'Printing Transparent/All Dependencies' command.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15946 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-11Improving rendering of ldots in doc (partially done, there are tooherbelin
much of them). Improving doc of conversion clauses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15733 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-03Document the command Add/Remove Search Blacklistletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15674 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
- For instance, refl_equal --> eq_refl - Npos, Zpos, Zneg now admit more uniform qualified aliases N.pos, Z.pos, Z.neg. - A new module BinInt.Pos2Z with results about injections from positive to Z - A result about Z.pow pushed in the generic layer - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l} - Using tactic Z.le_elim instead of Zle_lt_or_eq - Some cleanup in ring, field, micromega (use of "Equivalence", "Proper" ...) - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp) - In ZMake and ZMake, functor parameters are now named NN and ZZ instead of N and Z for avoiding confusions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-23Documentation of last commit concerning Backtrackingletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15086 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-23Remove old proof-managment commands Suspend/Resumeletouzey
There're not compatible with the current Backtrack mecanism used both by ProofGeneral and CoqIDE. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15083 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Bug 2583: Update of the syntax of terms in the reference manualpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14425 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 00:55:07 +0000