coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[build] Remove coqmktop in favor of ocamlfind.	Emilio Jesus Gallego Arias	2017-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.	Pierre-Marie Pédrot	2017-12-01
\|
*	Documenting the possibility to pass filenames to coqchk.	Pierre-Marie Pédrot	2017-11-29
\|
*	Remove GeoProof support.	Maxime Dénès	2017-10-11
\| \| \| \| \|	Julien Narboux confirmed that it was dead code (GeoProof is not to be confused with GeoCoq).
*	Typo in coqdep man	Gaëtan Gilbert	2017-09-29
\|
*	[flags] Remove XML output flag.	Emilio Jesus Gallego Arias	2017-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.	Emilio Jesus Gallego Arias	2017-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.	Maxime Dénès	2016-01-15
\|
*	Fix #4408.	Pierre Courtieu	2016-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.	Guillaume Melquiond	2015-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.	Pierre-Marie Pédrot	2015-09-25
\|
*	Updating the documentation and the toolchain w.r.t. the change in -compile.	Pierre-Marie Pédrot	2015-09-25
\|
*	Removing dead code relative to the XML plugin.	Pierre-Marie Pédrot	2014-09-08
\|
*	Removing documentation related to the deprecated State machinery.	Pierre-Marie Pédrot	2014-08-16
\|
*	Deprecate useless option -quality.	Guillaume Melquiond	2014-06-13
\|
*	Remove documentation for the unsupported options -byte and -opt.	Guillaume Melquiond	2014-06-13
\|
*	Coqdep always uses / as dir_sep	Pierre Boutillier	2013-12-20
\|
*	Coqtop and coqc: cleaning description of options in RefMan and manpages.	pboutill	2012-01-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14934 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix typo	glondu	2012-01-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14889 85f007b7-540e-0410-9357-904b9bb8a0f7
*	-user option removal	pboutill	2011-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 -coqlib	barras	2011-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)	letouzey	2011-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 coqmktop	glondu	2011-01-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13789 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix typos	glondu	2010-06-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13053 85f007b7-540e-0410-9357-904b9bb8a0f7
*	splitted -> split	glondu	2010-02-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12722 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fix coqchk options documentation	barras	2009-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.	herbelin	2009-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 stuff	letouzey	2009-03-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11975 85f007b7-540e-0410-9357-904b9bb8a0f7
*	man page of coqchk	barras	2009-02-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11901 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renaming parser -> coq-parser	glondu	2008-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)	glondu	2008-08-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11324 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Various fixes in manpages	glondu	2008-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 -slash	barras	2006-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 coq	notin	2006-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. ↵	notin	2006-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 coqdoc	notin	2006-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)	coq	2006-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.	sacerdot	2004-03-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5603 85f007b7-540e-0410-9357-904b9bb8a0f7
*	page de man pour coqdoc	filliatr	2004-03-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5501 85f007b7-540e-0410-9357-904b9bb8a0f7
*	page de man pour coqwc	filliatr	2004-03-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5500 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3862 85f007b7-540e-0410-9357-904b9bb8a0f7
*	application patch Claudio	filliatr	2001-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 parser	courant	2001-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 coqmktop	courant	2001-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.byte	courant	2001-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