coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Removing non-marshallable data from the Agram constructor. Instead of	Pierre-Marie Pédrot	2014-02-16
*	Getting rid of goal-dependency in declarative mode argument evaluation.	Pierre-Marie Pédrot	2013-11-27
*	Adds a new goal selector "all:".	aspiwack	2013-11-02
*	Cleanup of comments.	aspiwack	2013-11-02
*	STM: better handle proof modes	gareuselesinge	2013-09-30
*	Vernac classification streamlined (handles VERNAC EXTEND)	gareuselesinge	2013-08-08
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Splitted up Genarg in four different levels:	ppedrot	2013-06-21
*	Revert "parse "of" as KEYID "of""	gareuselesinge	2013-06-21
*	parse "of" as KEYID "of"	gareuselesinge	2013-06-19
*	Removing the various glob/subst/interp registering functions for	ppedrot	2013-06-18
*	Uniformizing generic argument types.	ppedrot	2013-06-06
*	No reason a priori for using unfiltered env for printing	herbelin	2013-01-29
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp	letouzey	2012-10-16
*	Moved Compat to parsing. This permits to break the dependency of the	ppedrot	2012-10-04
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	Updating headers.	herbelin	2012-08-08
*	place all files specific to camlp4 syntax extensions in grammar/	letouzey	2012-05-29
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
*	Corrects a (very) longstanding bug of tactics. As is were, tactic expecting	aspiwack	2012-04-18
*	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin	2012-03-20
*	Fixing bug #2732 (anomaly when using the tolerance for writing	herbelin	2012-03-18
*	Noise for nothing	pboutill	2012-03-02
*	Moving bullets (-, +, *) into stand-alone commands instead of being	courtieu	2011-12-16
*	Revert "Check if recursive calls are guarded before printing "Proof completed"."	pboutill	2011-06-10
*	Check if recursive calls are guarded before printing "Proof completed".	herbelin	2011-05-26
*	Made the emacs-U option deprecated. Also removed the old code	courtieu	2011-05-24
*	Fixed a bug causing inconsistent states during proof editting.	aspiwack	2011-04-29
*	Declarative mode: fix escape and return.	aspiwack	2011-04-19
*	Fixes the weird bug of the declarative proof mode (Czar) both in emacs and coqc.	aspiwack	2011-04-06
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey	2010-05-19
*	static (and shared) camlp4use instead of per-file declaration	letouzey	2010-05-19
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22