coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
*	Removing dead code relative to the XML plugin.	Pierre-Marie Pédrot	2014-09-08
*	Continuing (incomplete) cleaning of Inductiveops.	Hugo Herbelin	2014-08-01
*	A tentative uniform naming policy in module Inductiveops.	Hugo Herbelin	2014-08-01
*	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
*	G_xml: remove some duplication in error fonctions	Pierre Letouzey	2014-01-30
*	G_xml: protect against some possible Not_found	Pierre Letouzey	2014-01-30
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Turn many List.assoc into List.assoc_f	letouzey	2013-10-24
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	Restrict (try...with...) to avoid catching critical exn (part 9)	letouzey	2013-03-13
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Modulification of identifier	ppedrot	2012-12-14
*	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
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	Glob_term now mli-only, operations now in Glob_ops	letouzey	2012-05-29
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Glob_term.predicate_pattern: No number of parameters with letins.	pboutill	2012-03-02
*	Noise for nothing	pboutill	2012-03-02
*	Inductiveops.nb_*{,_env} cleaning	pboutill	2012-01-16
*	Allow "\|_=>_" in "match" in patterns, no more forced enumeration of constructors	letouzey	2011-11-07
*	More {raw => glob} changes for consistency	glondu	2010-12-24
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	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
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Some dead code removal + cleanups	letouzey	2009-04-08
*	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau	2009-03-28
*	Uniformisation du format des messages d'erreur (commencent par une	herbelin	2008-07-17
*	- Second pass on implementation of let pattern. Parse "let ' par [as x]?	msozeau	2008-03-28
*	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau	2007-12-31
*	Generalized CAMLP4USE for pp dependencies	corbinea	2007-07-16
*	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau	2007-03-19
*	le parsing du LETIN ne suivait pas la DTD (bug #1237)	herbelin	2006-10-03
*	Nettoyage code mort	herbelin	2006-07-05
*	Added {measure x f} as a valid recursion order.	msozeau	2006-06-22
*	The "clean integration of subtac" patch.	msozeau	2006-05-29
*	- Distinction explicite des parties paramètres et arguments dans le type	herbelin	2006-04-27
*	- Utilisation d'abbréviations pour les types intervenant dans RCases	herbelin	2006-04-26
*	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey	2006-04-14