coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing compatibility layers related to printing.	Pierre-Marie Pédrot	2017-02-14
*	Goal API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Moving Ltac-specific parsing API to ltac/ folder.	Pierre-Marie Pédrot	2016-09-14
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Merge remote-tracking branch 'origin/pr/173' into trunk	Enrico Tassi	2016-06-14
\|\
* \|	Compilation via pack for plugins of the stdlib	Pierre Letouzey	2016-06-08
\| *	STM: proof block detection/error resilience API	Enrico Tassi	2016-06-06
\|/
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-04
\|\
\| *	Remove extraneous space in coqtop/pg output (bug #4675).	Guillaume Melquiond	2016-05-03
* \|	Moving the proof mode parsing management to Pcoq.	Pierre-Marie Pédrot	2016-03-19
* \|	Adding a universe argument to Pcoq.create_generic_entry.	Pierre-Marie Pédrot	2016-03-17
* \|	Removing the registering of default values for generic arguments.	Pierre-Marie Pédrot	2016-03-17
\|/
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Declarative mode: fix vernac classification.	Arnaud Spiwack	2015-03-31
*	Declarative mode: plug the specialised printers back.	Arnaud Spiwack	2015-03-31
*	rewiring Czar printers that were disabled	Pierre Corbineau	2015-03-13
*	Fix double print in decl_mode.	Enrico Tassi	2015-03-11
*	Update headers.	Maxime Dénès	2015-01-12
*	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin	2014-09-12
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
*	STM: new "par:" goal selector, like "all:" but in parallel	Enrico Tassi	2014-08-05
*	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