coq - The formal proof system

Age	Commit message (Expand)	Author
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2012-12-14	Modulification of dir_path	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-12-13	Renamed Option.Misc.compare to the more uniform Option.equal.	ppedrot
2012-11-25	Monomorphization (interp)	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-11-13	Added a CString module.	ppedrot
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	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia
2012-08-08	Updating headers.	herbelin
2012-07-30	Bigint: avoid dependency over Pp	letouzey
2012-07-05	Open Scope can now also accepts delimiters (e.g. Z).	letouzey
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-06-14	Internalization of pattern is done in two phases.	pboutill
2012-06-04	Replacing some str with strbrk	ppedrot
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey
2012-05-29	Stuff about notation_constr (ex-aconstr) now in notation_ops.ml	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-15	Notations are back in the "in" clause of pattern matching.	pboutill
2012-03-26	Slight change in the semantics of arguments scopes: scopes can no	herbelin
2012-03-20	Continuing r15045-15046 and r15055 (fixing bug #2732 about atomic	herbelin
2012-03-02	Noise for nothing	pboutill
2012-01-05	Backtracking on r14876 (fix for bug #2267): extra scopes might be	herbelin
2012-01-04	Fixing Arguments Scope bug when too many scopes are given (bug #2667).	herbelin
2011-12-18	Fixing bug #2634 (unscoped notations were disturbing the	herbelin
2011-12-17	A pass on warning printings. Made systematic the use of msg_warning so	herbelin
2011-11-02	Add type annotations around all calls to Libobject.declare_object	letouzey
2011-03-31	Did that adding a rule for printing applications as "f(x)" works.	herbelin
2011-03-05	Added a table for using reserved names for binding names to types	herbelin
2011-02-12	fix last commit about modules (subst_cl_typ may raise Not_found)	letouzey
2011-02-11	An automatic substitution of scope at functor application	letouzey
2011-02-11	Annotations at functor applications:	letouzey
2010-12-24	More {raw => glob} changes for consistency	glondu
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-12-23	Change of nomenclature: rawconstr -> glob_constr	glondu
2010-09-24	Partial review of removed dead code (r13460)	herbelin
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-07-22	Extension of the recursive notations mechanism	herbelin
2010-06-08	Fixed wrong spelling in a warning.	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-10	Optimized need for delimiters when disjoint scopes for strings and	herbelin
2010-03-29	Several bug-fixes and improvements of coqdoc	herbelin
2009-11-02	list, length, app are migrated from List to Datatypes	letouzey
2009-10-26	Local/Global revision 12418 continued	herbelin
2009-10-26	New cleaning phase of the Local/Global option management	herbelin
2009-10-25	Improved the treatment of Local/Global options (noneffective Local on	herbelin