coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	STM: fix for PG and "Proof term" lines.	gareuselesinge	2013-11-05
*	Fixes parsing of all: followed by a typechecking/evaluation command.	aspiwack	2013-11-02
*	Adds a new goal selector "all:".	aspiwack	2013-11-02
*	STM: add "Stm Wait" to wait for the slaves to complete their jobs	gareuselesinge	2013-10-10
*	STM: new command "Stm PrintDag" to force printing the dag to /tmp	gareuselesinge	2013-10-07
*	STM: better handle proof modes	gareuselesinge	2013-09-30
*	Modulification and removing of structural equality in Stateid.	ppedrot	2013-08-19
*	stm: (initial) support for -coq-slaves	gareuselesinge	2013-08-08
*	Vernac classification streamlined (handles VERNAC EXTEND)	gareuselesinge	2013-08-08
*	Support Proof General	gareuselesinge	2013-08-08
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Added a Print Debug GC command that displays the current state of	ppedrot	2013-08-01
*	Granting bug #3098: adding priority to Existing Instances.	ppedrot	2013-08-01
*	More dynamic argument scopes	letouzey	2013-07-17
*	Added a Register Inline command for the native compiler. Will be ported to th...	mdenes	2013-07-10
*	More comments in Genarg.	ppedrot	2013-06-06
*	More functional implementation of locality_flag and program_mode	gareuselesinge	2013-04-15
*	Modules and ppvernac, sequel of Enrico's commit 16261	letouzey	2013-03-13
*	Allowing (Co)Fixpoint to be defined local and Let-style.	ppedrot	2013-03-11
*	Added a Local Definition vernacular command. This type of definition	ppedrot	2013-03-11
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Useless use of hooks in VernacDefinition. In addition, this was	ppedrot	2013-02-10
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Change [Hints Resolve] to still accept constrs as arguments	msozeau	2012-10-31
*	Fixed #2926:	ppedrot	2012-10-29
*	Change Hint Resolve, Immediate to take a global reference as argument	msozeau	2012-10-26
*	Moved Compat to parsing. This permits to break the dependency of the	ppedrot	2012-10-04
*	Added support for option Local (at module level) in Tactic Notation.	herbelin	2012-08-11
*	Updating headers.	herbelin	2012-08-08
*	A prototype implementation of a Print Namespace command.	aspiwack	2012-07-06
*	Notation: a new annotation "compat 8.x" extending "only parsing"	letouzey	2012-07-05
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Vernacexpr is now a mli-only file, locality stuff now in locality.ml	letouzey	2012-05-29