coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	Partly replacing list-based access functions in Evd. This is still	ppedrot	2013-09-03
*	Modulification and removing of structural equality in Stateid.	ppedrot	2013-08-19
*	Coqide ported to STM	gareuselesinge	2013-08-08
*	State Transaction Machine	gareuselesinge	2013-08-08
*	New module Xml_printer (dual to Xml_parser)	gareuselesinge	2013-05-06
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	raise UnsafeSuccess -> feedback AddedAxiom	gareuselesinge	2013-04-25
*	Coqide: new feedback mechanism for structured content	gareuselesinge	2013-04-25
*	interface.mli and serialize.ml reworked to avoid copy/paste of types	gareuselesinge	2013-04-19
*	More functional implementation of locality_flag and program_mode	gareuselesinge	2013-04-15
*	Moved the Loadpath part of Library to its own file, and documented	ppedrot	2013-03-26
*	Vernac+Toplevel: get rid of Error_in_file	letouzey	2013-03-13
*	Vernac+Toplevel: get rid of DuringVernacInterp	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 13)	letouzey	2013-03-13
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Removing Exc_located and using the new exception enrichement	ppedrot	2013-02-18
*	Ide_slave: do not prepare debug messages in non-debug mode	letouzey	2012-12-17
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Removed Compat.Exc_located outside of compat.ml4, as a consequence of	herbelin	2012-12-04
*	Monomorphization (toplevel)	ppedrot	2012-11-26
*	Ide_slave: do not attempt to answer broken requests	letouzey	2012-11-12
*	Xml_parser: detect immediate EOF + disable check_eof by default	letouzey	2012-11-12
*	Text inserted by insert_this_phrase_on_success correct tagging	pboutill	2012-10-23
*	Moved Compat to parsing. This permits to break the dependency of the	ppedrot	2012-10-04
*	Partial revert of Yann commit in order to use CLib.List when opening	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Let coqtop be a little more stupid in hint answer: otherwise, that	ppedrot	2012-07-20
*	A new status Unsafe in Interface. Meant for commands such as Admitted.	aspiwack	2012-07-12
*	Adapting the IDE interface with the focussed display.	ppedrot	2012-07-10
*	Moved code out of ide_slave in a more appropriate place.	ppedrot	2012-07-09
*	Various small display improvement	ppedrot	2012-06-29
*	Small improvement to ide_slave, which was going crazy whenever	ppedrot	2012-06-29
*	Now CoqIDE separates answer and messages. This should hopefully	ppedrot	2012-06-29
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	Replacing some str with strbrk	ppedrot	2012-06-04
*	Added a color output to Coqtop.	ppedrot	2012-06-04
*	Separated notice vs info messages, and cleaned up the interface a bit.	ppedrot	2012-06-04
*	Vernacexpr is now a mli-only file, locality stuff now in locality.ml	letouzey	2012-05-29
*	Added a SearchAbout-like primitive in coqtop interface.	ppedrot	2012-05-13
*	Added an interface primitive to ask coqtop for its internal versions.	ppedrot	2012-05-13
*	Slightly modified the coqtop interface by adding an identifier in	ppedrot	2012-05-11
*	Added an interface call to exit Coqtop nicely.	ppedrot	2012-05-02
*	lib directory is cut in 2 cma.	pboutill	2012-04-12
*	A unified backtrack mechanism, with a basic "Show Script" as side-effect	letouzey	2012-03-23
*	Remove undocumented command "Delete foo"	letouzey	2012-03-23
*	Remove old proof-managment commands Suspend/Resume	letouzey	2012-03-23
*	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin	2012-03-20