aboutsummaryrefslogtreecommitdiffhomepage
path: root/man
Commit message (Collapse)AuthorAge
* Add CHANGES and man entry for coqdep learning _CoqProject.Gravatar Gaëtan Gilbert2018-03-06
|
* [build] Remove coqmktop in favor of ocamlfind.Gravatar Emilio Jesus Gallego Arias2017-12-10
| | | | | | | | | | | | | | | | | 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.
* Documenting the -Q flag of coqchk.Gravatar Pierre-Marie Pédrot2017-12-01
|
* Documenting the possibility to pass filenames to coqchk.Gravatar Pierre-Marie Pédrot2017-11-29
|
* Remove GeoProof support.Gravatar Maxime Dénès2017-10-11
| | | | | Julien Narboux confirmed that it was dead code (GeoProof is not to be confused with GeoCoq).
* Typo in coqdep manGravatar Gaëtan Gilbert2017-09-29
|
* [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
| | | | | | | | 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.
* [vernac] Remove `Save.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
| | | | It has been deprecated for a while in favor of `Qed`.
* Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
|
* Fix #4408.Gravatar Pierre Courtieu2016-01-15
| | | | | Removed documentation for broken -D -w (but the option are still there). Fixed documentation of others.
* Make -load-vernac-object respect the loadpath.Gravatar Guillaume Melquiond2015-09-28
| | | | | | | | | | 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.
* The -require option now accepts a logical path instead of a physical one.Gravatar Pierre-Marie Pédrot2015-09-25
|
* Updating the documentation and the toolchain w.r.t. the change in -compile.Gravatar Pierre-Marie Pédrot2015-09-25
|
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
|
* Removing documentation related to the deprecated State machinery.Gravatar Pierre-Marie Pédrot2014-08-16
|
* Deprecate useless option -quality.Gravatar Guillaume Melquiond2014-06-13
|
* Remove documentation for the unsupported options -byte and -opt.Gravatar Guillaume Melquiond2014-06-13
|
* Coqdep always uses / as dir_sepGravatar Pierre Boutillier2013-12-20
|
* Coqtop and coqc: cleaning description of options in RefMan and manpages.Gravatar pboutill2012-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14934 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix typoGravatar glondu2012-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14889 85f007b7-540e-0410-9357-904b9bb8a0f7
* -user option removalGravatar pboutill2011-11-21
| | | | | | | 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
* fixed coqchk usage and man page + added option -coqlibGravatar barras2011-07-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14264 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove old traces of SearchIsos (never ported to 7.x nor 8.x)Gravatar letouzey2011-04-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13986 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove references to -ide option of coqmktopGravatar glondu2011-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13789 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix typosGravatar glondu2010-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13053 85f007b7-540e-0410-9357-904b9bb8a0f7
* splitted -> splitGravatar glondu2010-02-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12722 85f007b7-540e-0410-9357-904b9bb8a0f7
* fix coqchk options documentationGravatar barras2009-12-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12552 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added option --external to coqdoc to bind an url to an external library.Gravatar herbelin2009-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12426 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdep: remove references to obsolete .zi and Require Implementation stuffGravatar letouzey2009-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11975 85f007b7-540e-0410-9357-904b9bb8a0f7
* man page of coqchkGravatar barras2009-02-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11901 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renaming parser -> coq-parserGravatar glondu2008-08-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11328 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add coqide manpage (taken from Debian)Gravatar glondu2008-08-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11324 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various fixes in manpagesGravatar glondu2008-08-08
| | | | | | | | * 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
* coqdep -slashGravatar barras2006-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9276 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de pages de man pour les exécutables coqGravatar notin2006-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9233 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une option --coqlib_path pour Coqdoc (modification suggérée par S. ↵Gravatar notin2006-05-02
| | | | | | Mimram) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8775 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la doc de l'option -stdout de coqdocGravatar notin2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8749 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding a man page for doqdoc (JMN)Gravatar coq2006-01-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7794 85f007b7-540e-0410-9357-904b9bb8a0f7
* tools/coq_vo2xml removed since no longer in use.Gravatar sacerdot2004-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5603 85f007b7-540e-0410-9357-904b9bb8a0f7
* page de man pour coqdocGravatar filliatr2004-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5501 85f007b7-540e-0410-9357-904b9bb8a0f7
* page de man pour coqwcGravatar filliatr2004-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5500 85f007b7-540e-0410-9357-904b9bb8a0f7
* TypoGravatar herbelin2003-04-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3862 85f007b7-540e-0410-9357-904b9bb8a0f7
* application patch ClaudioGravatar filliatr2001-05-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1746 85f007b7-540e-0410-9357-904b9bb8a0f7
* man pages for coq-interface and parserGravatar courant2001-04-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1717 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout pages de man coq_makefile et coqmktopGravatar courant2001-04-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1716 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Ajout pages de man pour coqc, coqtop, coqtop.opt et coqtop.byteGravatar courant2001-04-25
- Deplacement pages de tools/ vers man/ - Modif distrib/Makefile pour Debian - Modif mode emacs pour Debian git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1710 85f007b7-540e-0410-9357-904b9bb8a0f7