aboutsummaryrefslogtreecommitdiff
path: root/man
AgeCommit message (Collapse)Author
2021-04-12[coqdep] error on non-existent and unreadable filesHendrik Tews
Print an error message and return non-zero status for non-existing or unreadable files. Unknown options produce a warning and are otherwise ignored. Fixes #14023
2021-03-28[coqdep] remove leftover Caml stuff from man pageHendrik Tews
Dependencies for Caml files was removed in PR #11589, but some parts of it survived in the man page.
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
We introduce a new package structure for Coq: - `coq-core`: Coq's OCaml tools code and plugins - `coq-stdlib`: Coq's stdlib [.vo files] - `coq`: meta-package that pulls `coq-{core,stdlib}` This has several advantages, in particular it allows to install Coq without the stdlib which is useful in several scenarios, it also open the door towards a versioning of the stdlib at the package level. The main user-visible change is that Coq's ML development files now live in `$lib/coq-core`, for compatibility in the regular build we install a symlink and support both setups for a while. Note that plugin developers and even `coq_makefile` should actually rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust. There is a transient state where we actually look for both `$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support the non-ocamlfind plus custom variables. This will be much improved once #13617 is merged (which requires this PR first), then, we will introduce a `coq.boot` library so finally `coqdep`, `coqchk`, etc... can share the same path setup code. IMHO the plan should work fine.
2020-05-10Remove (outdated) timestamps from man pagesKartik Singhal
2020-04-02Minimal fix to man pages.Théo Zimmermann
2020-02-17Merge PR #11593: Update bug report address in coqwc man page.Théo Zimmermann
Reviewed-by: Zimmi48
2020-02-13[coqdep] Remove support for `-c` ocamldep replacement.Emilio Jesus Gallego Arias
There is not need for coqdep to ship an `ocamldep` replacement, in particular: - not used in the main build since a long time - not tested - not kept up to date with upstream This allows for a significant reduction of `coqdep` code, including some duplicated code from `ocamllibdep`. `coq_makefile` now uses `ocamllibdep` to process `mllib/mlpack` files, so it has then to be installed. We also remove the residual `-slash` option.
2020-02-13Update bug report address in coqwc man page.Gaëtan Gilbert
2020-02-07[coqdep] Remove dumpgraph and broken optionsEmilio Jesus Gallego Arias
We remove the `dumpgraph` option which was causing quite a bit of duplication, we also clean up options marked as broken `-w/-D`
2019-11-21Document -vos flag for coqdepGaëtan Gilbert
2019-05-23Fixing typos - Part 2JPR
2019-02-22[library] Remove `-boot` option.Emilio Jesus Gallego Arias
The `-boot` option was used to: - suppress loading of the rc_file - allow to save modules with prefix `Coq` There is no good reason disable saving of modules with `Coq` prefix by default, thus we remove this option. Fixes: #9575
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
This PR deprecates the use of `coqtop` as a compiler. There is no point on having two binaries with the same purpose; after the experiment in #8690, IMHO we have a lot to gain in terms of code organization by splitting the compiler and the interactive binary. We adapt the documentation and adapt the test-suite. Note that we don't make `coqc` a true binary yet, but here we take care only of the user-facing part. The conversion of the binary will take place in #8690 and will bring code simplification, including a unified handling of arguments.
2018-10-23[dune] Install man pages + remove two obsolete ones.Emilio Jesus Gallego Arias
2018-06-25Archive the `gallina` toolVincent Laporte
2018-05-16Minor update of the documentation/man about the resource file.Hugo Herbelin
2018-03-06Add CHANGES and man entry for coqdep learning _CoqProject.Gaëtan Gilbert
2017-12-10[build] Remove coqmktop in favor of ocamlfind.Emilio Jesus Gallego Arias
We remove coqmktop in favor of a couple of simple makefile rules using ocamlfind. In order to do that, we introduce a new top-level file that calls the coqtop main entry. This is very convenient in order to use other builds systems such as `ocamlbuild` or `jbuilder`. An additional consideration is that we must perform a side-effect on init depending on whether we have an OCaml toplevel available [byte] or not. We do that by using two different object files, one for the bytecode version other for the native one, but we may want to review our choice. We also perform some smaller cleanups taking profit from ocamlfind.
2017-12-01Documenting the -Q flag of coqchk.Pierre-Marie Pédrot
2017-11-29Documenting the possibility to pass filenames to coqchk.Pierre-Marie Pédrot
2017-10-11Remove GeoProof support.Maxime Dénès
Julien Narboux confirmed that it was dead code (GeoProof is not to be confused with GeoCoq).
2017-09-29Typo in coqdep manGaëtan Gilbert
2017-08-01[flags] Remove XML output flag.Emilio Jesus Gallego Arias
This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied.
2017-05-23[vernac] Remove `Save.` command.Emilio Jesus Gallego Arias
It has been deprecated for a while in favor of `Qed`.
2016-01-15Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Maxime Dénès
2016-01-15Fix #4408.Pierre Courtieu
Removed documentation for broken -D -w (but the option are still there). Fixed documentation of others.
2015-09-28Make -load-vernac-object respect the loadpath.Guillaume Melquiond
This command-line option was behaving like the old -require, except that it did not do Import. In other words, it was loading files without respecting the loadpath. Now it behaves exactly like Require, while -require now behaves like Require Import. This patch also removes Library.require_library_from_file and all its dependencies, since they are no longer used inside Coq.
2015-09-25The -require option now accepts a logical path instead of a physical one.Pierre-Marie Pédrot
2015-09-25Updating the documentation and the toolchain w.r.t. the change in -compile.Pierre-Marie Pédrot
2014-09-08Removing dead code relative to the XML plugin.Pierre-Marie Pédrot
2014-08-16Removing documentation related to the deprecated State machinery.Pierre-Marie Pédrot
2014-06-13Deprecate useless option -quality.Guillaume Melquiond
2014-06-13Remove documentation for the unsupported options -byte and -opt.Guillaume Melquiond
2013-12-20Coqdep always uses / as dir_sepPierre Boutillier
2012-01-21Coqtop and coqc: cleaning description of options in RefMan and manpages.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14934 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-07Fix typoglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14889 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21-user option removalpboutill
it is imcompatible with the freedesktop policy that config directory is private. Feel absolutly free to revert this commit if you think -user should stay git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14713 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-07fixed coqchk usage and man page + added option -coqlibbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14264 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-12remove old traces of SearchIsos (never ported to 7.x nor 8.x)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13986 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-11Remove references to -ide option of coqmktopglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13789 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-02Fix typosglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13053 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-10splitted -> splitglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12722 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-01fix coqchk options documentationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12552 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-27Added option --external to coqdoc to bind an url to an external library.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12426 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-14Coqdep: remove references to obsolete .zi and Require Implementation stuffletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11975 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-10man page of coqchkbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11901 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-18Renaming parser -> coq-parserglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11328 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-12Add coqide manpage (taken from Debian)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11324 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-08Various fixes in manpagesglondu
* hyphen meant as the ascii character should be escaped * lines starting with a dot have a special meaning git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11322 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-25coqdep -slashbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9276 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:08:11 +0000