coq - The formal proof system

Age	Commit message (Expand)	Author
2011-12-12	Proof using ...	gareuselesinge
2011-11-18	Restore backward compatibility. ":>" declares subinstances in Class declarati...	msozeau
2011-11-17	Merge subinstances branch by me and Tom Prince.	msozeau
2011-06-14	Fixing bug #2181 (Class mechanism can create dependencies over unnamed	herbelin
2011-04-13	Revert "Add [Polymorphic] flag for defs"	msozeau
2011-04-13	Add [Polymorphic] flag for defs	msozeau
2011-03-13	- Add modulo_delta_types flag for unification to allow full	msozeau
2011-03-11	Keep information on which fields are subclasses in class declarations,	msozeau
2011-02-10	Interp a definition with the implicit arguments of its local context	pboutill
2011-02-10	Data structure telling implicits of local variables is a map in the	pboutill
2011-01-28	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey
2010-12-24	More {raw => glob} changes for consistency	glondu
2010-11-18	Do not throw an error for anonymous generalized binders as they will be	msozeau
2010-11-15	Minor fixes from Gregory Malecha. A typo fixed and a better (located)	msozeau
2010-10-03	Added multiple implicit arguments rules per name.	herbelin
2010-09-28	Fix bug #2321, allowing "_" named projections in classes. Not realizing	msozeau
2010-09-28	Remove some occurrences of "open Termops"	glondu
2010-09-28	Fix function applications without labels (OCaml warning 6)	glondu
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-09-02	* removed declare_constant and declare_internal_constant	vsiles
2010-09-02	v13392 port from v8.3 to trunk : correct message when defining inductive schemes	vsiles
2010-07-24	Updated all headers for 8.3 and trunk	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-06-29	change the flag "internal" in declare/ind_tables from bool to	vsiles
2010-06-12	Fixing spelling: pr_coma -> pr_comma	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-03-07	Fix treatment of remaining unification constraints: raise a more	msozeau
2009-11-11	Added support for multiple where-clauses in Inductive and co (see wish #2163).	herbelin
2009-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin
2009-11-08	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-07-07	Jolification : tentative de supprimer les "( evd)" et associés qui	aspiwack
2009-05-13	Fix to my last notation patch: now fixpoint are correctly handled	vsiles
2009-05-09	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin
2009-04-24	Backporting 12080 (fixing bug #2091 on bad rollback in the "where"	herbelin
2009-03-28	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau
2009-02-19	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack
2009-01-19	Les records déclarés avec Record ne peuvent plus être récursifs (le	aspiwack
2009-01-17	DISCLAIMER	puech
2008-12-31	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin
2008-12-14	Generalized binding syntax overhaul: only two new binders: `() and `{},	msozeau
2008-11-23	Fixed bug #2006 (type constraint on Record was not taken into account) +	herbelin
2008-11-10	Fix mixup between Record, Structure and Class by adding a new variant for	msozeau
2008-11-09	More factorization of inductive/record and typeclasses: move class	msozeau
2008-11-05	Move Record desugaring to constrintern and add ability to use notations	msozeau
2008-11-05	Nouvelle syntaxe pour écrire des records (co)inductifs :	aspiwack
2008-10-08	Fix bug #1959 (remember: never use a partial functions mindlessly).	msozeau
2008-09-14	In manual implicit arguments mode, do not enrich implicits	msozeau