coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-05-10	Remove (outdated) timestamps from man pages	Kartik Singhal

2020-04-02	Minimal fix to man pages.	Théo Zimmermann

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-05-16	Minor update of the documentation/man about the resource file.	Hugo Herbelin

2017-10-11	Remove GeoProof support.	Maxime Dénès
	Julien Narboux confirmed that it was dead code (GeoProof is not to be confused with GeoCoq).
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.
2016-01-15	Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.	Maxime Dénès

2015-09-28	Make -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-25	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

2014-09-08	Removing dead code relative to the XML plugin.	Pierre-Marie Pédrot

2014-08-16	Removing documentation related to the deprecated State machinery.	Pierre-Marie Pédrot

2014-06-13	Deprecate useless option -quality.	Guillaume Melquiond

2014-06-13	Remove documentation for the unsupported options -byte and -opt.	Guillaume Melquiond

2012-01-21	Coqtop 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-07	Fix typo	glondu
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14889 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-11	Ajout de pages de man pour les exécutables coq	notin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9233 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-25	man pages for coq-interface and parser	courant
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1717 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-25	Ajout pages de man coq_makefile et coqmktop	courant
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1716 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-25	- Ajout pages de man pour coqc, coqtop, coqtop.opt et coqtop.byte	courant
	- 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