coq - The formal proof system

Age	Commit message (Expand)	Author
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-09-14	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot
2012-09-14	This patch removes unused "open" (automatically generated from	regisgia
2012-08-08	Updating headers.	herbelin
2012-06-04	Separated notice vs info messages, and cleaned up the interface a bit.	ppedrot
2012-06-01	Cleaning Pp.ppnl use	ppedrot
2012-06-01	Getting rid of Pp.msgnl and Pp.message.	ppedrot
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey
2012-05-29	Basic stuff about constr_expr migrated from topconstr to constrexpr_ops	letouzey
2012-05-29	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey
2012-05-29	Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml	letouzey
2012-04-13	Better error message when defining recursive records with Record or	aspiwack
2012-03-14	Second step of integration of Program:	msozeau
2012-03-02	Noise for nothing	pboutill
2012-01-25	Check for unresolved evars in textual order of the params and fields declarat...	msozeau
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