coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Properly declare uconstr as an argument for TACTIC EXTEND.	Arnaud Spiwack	2014-08-05
*	Fixing #3390 (mismatch simple_tactic/tactic0 leading to segfault).	Hugo Herbelin	2014-06-21
*	Adding way to get the list of the accepted tactic notation arguments.	Pierre-Marie Pédrot	2014-05-17
*	Closing bug #3260	Julien Forest	2014-04-14
*	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
*	Removing the useless pattern ident genarg.	Pierre-Marie Pédrot	2013-12-19
*	Getting rid of casted_open_constr. It was only used by the	Pierre-Marie Pédrot	2013-11-30
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Expurgating the useless difference between List0 and List1 at the	ppedrot	2013-07-05
*	Removing the use of leveled tactics wit_tacticn. It is now handled	ppedrot	2013-07-02
*	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot	2013-06-21
*	Proof-of-concept: moved four easy-to-handle generic arguments to	ppedrot	2013-06-18
*	Uniformizing generic argument types.	ppedrot	2013-06-06
*	avoid (Int.equal (cmp ...) 0) when a boolean equality exists	letouzey	2013-02-19
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Monomorphization (parsing)	ppedrot	2012-11-25
*	More monomorphizations	ppedrot	2012-11-13
*	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
*	More cleaning on Utils and CList. Some parts of the code being	ppedrot	2012-09-17
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Two adaptations after the changes of level of ->	letouzey	2012-07-06
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	Migrate the grammar entry about "Ltac" into g_vernac.ml4.	letouzey	2012-05-29
*	Noise for nothing	pboutill	2012-03-02
*	Reverted previous commit, which broke library compilation.	ppedrot	2012-01-20
*	This is a quick hack to permit the parsing of the locality flag in the Progra...	ppedrot	2012-01-20
*	Oversight in revision 14292.	pboutill	2011-07-27
*	Pcoq.ml4: fix a typo in a comment to please ocamldoc	letouzey	2011-04-26
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	adapt slighlty r13642 to support both camlp4 and camlp5-5 and camlp5-6	letouzey	2010-11-18
*	Support for camlp5 6.02.0 (Closes: #2432)	glondu	2010-11-16
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Extension of the recursive notations mechanism	herbelin	2010-07-22
*	Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).	herbelin	2010-07-22
*	Using vernac parsing for Function	jforest	2010-06-08
*	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey	2010-05-19
*	Nicer representation of tokens, more independant of camlp*	letouzey	2010-05-19
*	static (and shared) camlp4use instead of per-file declaration	letouzey	2010-05-19
*	Discontinue support for ocaml 3.09.*	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
*	Several bug-fixes and improvements of coqdoc	herbelin	2010-03-29
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Generalized the possibility to refer to a global name by a notation	herbelin	2009-09-11
*	=?utf-8?q?D=C3=A9sinterdiction=20de=20GDELETE=5FRULE=20dans=20pcoq.ml4.=20Mal...	aspiwack	2009-05-27
*	- Fixed a little bug in previous commit (bad failure in case of unknown entry).	herbelin	2009-04-27