coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
*	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
*	romega: add a tactic named unsafe_romega (for debugging, or bold users)	Pierre Letouzey	2017-05-22
*	Removing trivial compatibility layer in refl_omega.	Pierre-Marie Pédrot	2017-04-24
*	Moving the Ltac plugin to a pack-based one.	Pierre-Marie Pédrot	2017-02-17
*	Merging Stdarg and Constrarg.	Pierre-Marie Pédrot	2016-09-21
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	Removing the special status of generic entries defined by Coq itself.	Pierre-Marie Pédrot	2016-03-17
*	Getting rid of the "<:tactic< ... >>" quotations.	Pierre-Marie Pédrot	2016-02-24
*	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey	2014-12-09
*	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot	2014-05-12
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	cList: a few alternative to hashtbl-based uniquize, distinct, subset	letouzey	2013-10-23
*	Modulification of identifier	ppedrot	2012-12-14
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	place all files specific to camlp4 syntax extensions in grammar/	letouzey	2012-05-29
*	Noise for nothing	pboutill	2012-03-02
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey	2009-03-20