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	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot
2012-09-14	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot
2012-08-08	Updating headers.	herbelin
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-06-01	Getting rid of Pp.msgnl and Pp.message.	ppedrot
2012-05-30	Getting rid of Pp.msg	ppedrot
2012-05-29	place all files specific to camlp4 syntax extensions in grammar/	letouzey
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	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey
2012-03-02	Noise for nothing	pboutill
2011-12-12	Proof using ...	gareuselesinge
2011-11-17	Fixing bug #2640 and variants of it (inconsistency between when and	herbelin
2011-11-02	Add type annotations around all calls to Libobject.declare_object	letouzey
2011-08-08	Esubst: make types of substitutions & lifts private	puech
2011-07-29	Newring: generic = on constr replaced by eq_constr	puech
2011-07-29	replaced some generic = on constr by eq_constr	puech
2011-07-29	Newring: replaced some generic = on constr by eq_constr	puech
2011-07-29	Newring: replaced generic = on constr by eq_constr	puech
2011-07-29	Newring: generic Pervasives.compare on constr replaced by constr_ord	puech
2011-07-29	Newring: generic equality on constr replaced by constr_equal	puech
2011-04-13	Revert "Add [Polymorphic] flag for defs"	msozeau
2011-04-13	Add [Polymorphic] flag for defs	msozeau
2011-01-28	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-12-23	Change of nomenclature: rawconstr -> glob_constr	glondu
2010-09-30	Simplify tactic(_)-bound arguments in TACTIC EXTEND rules	glondu
2010-09-28	Remove some occurrences of "open Termops"	glondu
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-09-19	Reverting partial fix for #2335 committed by mistake in r13435. Sorry.	herbelin
2010-09-19	Patch solving the bug but leaving open design choices	herbelin
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-06-06	Added support for Ltac-matching terms with variables bound in the pattern	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-22	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack
2010-03-05	Improvements in generalized rewriting:	msozeau
2010-01-28	New command Declare Reduction <id> := <conv_expr>.	letouzey
2009-10-21	This big commit addresses two problems:	soubiran
2009-09-17	Remove useless Liboject.export_function field	glondu
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-11	Generalized the possibility to refer to a global name by a notation	herbelin
2009-09-02	Stop unnecessary use of lazy values for constraints, simplifying	msozeau
2009-08-13	Death of "survive_module" and "survive_section" (the first one was	herbelin
2009-08-06	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin
2009-04-07	Move setoid_rewrite to its own module and do some clean up in	msozeau
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey