coq - The formal proof system

Age	Commit message (Expand)	Author
2014-05-06	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2013-12-22	Notations can now accept dummy arguments. If ever a bound variable is not	Pierre-Marie Pédrot
2013-12-17	Removing the need of evarmaps in constr internalization.	Pierre-Marie Pédrot
2013-09-02	Removing more association lists in Constrintern.	ppedrot
2013-08-03	Replacing uses of association lists by maps in notations.	ppedrot
2013-06-25	Useless use of maps in constr internalizing.	ppedrot
2013-05-09	A uniformization step around understand_* and interp_* functions.	herbelin
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-02-19	Dir_path --> DirPath	letouzey
2012-12-18	Modulification of name	ppedrot
2012-12-14	Modulification of dir_path	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-12-14	Implemented a full-fledged equality on [constr_expr]. By the way,	ppedrot
2012-11-25	More equality functions	ppedrot
2012-11-17	Taking into account the type of a definition (if it exists), and the	herbelin
2012-08-08	Updating headers.	herbelin
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey
2012-05-29	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	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-01-20	Added new command "Set Parsing Explicit" for deactivating parsing (and	herbelin
2011-02-10	Interp a definition with the implicit arguments of its local context	pboutill
2011-02-10	local variables can have implicits locally	pboutill
2011-02-10	Data structure telling implicits of local variables is a map in the	pboutill
2011-02-10	More comments and less doublons in some mli	pboutill
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-12-23	Change of nomenclature: rawconstr -> glob_constr	glondu
2010-10-03	Added multiple implicit arguments rules per name.	herbelin
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-07-22	Extension of the recursive notations mechanism	herbelin
2010-07-22	Simplified the way internalization_data (i.e. bindings of bound vars	herbelin
2010-07-22	Constrintern: unified push_name_env and push_loc_name_env; made	herbelin
2010-07-22	Switch to American spelling for "internalise" and "internalisation"	herbelin
2010-06-22	New script dev/tools/change-header to automatically update Coq files headers.	herbelin
2010-04-29	Various minor improvements of comments in mli for ocamldoc	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-29	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill
2010-01-28	Backport fixes in Instance declarations to Program Instance.	msozeau
2009-11-11	Promote evar_defs to evar_map (in Evd)	glondu
2009-11-11	Improving abbreviations/notations + backtrack of semantic change in r12439	herbelin
2009-11-08	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-06-18	Use more consistent resolution parameters in Program and regular typing	msozeau
2009-03-28	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau
2009-01-17	DISCLAIMER	puech
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-11-09	More factorization of inductive/record and typeclasses: move class	msozeau