coq - The formal proof system

Age	Commit message (Expand)	Author
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-30	More uniformisation in Pp.warn functions.	ppedrot
2012-05-29	remove many excessive open Util & Errors in mli's	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-05-29	Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml	letouzey
2012-04-12	lib directory is cut in 2 cma.	pboutill
2012-03-26	Module names and constant/inductive names are now in two separate namespaces	letouzey
2012-03-23	A unified backtrack mechanism, with a basic "Show Script" as side-effect	letouzey
2012-03-23	Remove undocumented command "Delete foo"	letouzey
2012-03-20	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin
2012-03-02	Noise for nothing	pboutill
2012-02-23	Implement the substitution function for global options. Fixes anomaly in ssre...	msozeau
2011-12-21	sequel of previous commit	letouzey
2011-12-21	Isolate a few types of Goptions in a pure .mli, solving a dep issue with ocam...	letouzey
2011-12-18	Fixed a Not_found bug when declaring in a section some implicit	herbelin
2011-12-17	A pass on warning printings. Made systematic the use of msg_warning so	herbelin
2011-12-12	Proof using ...	gareuselesinge
2011-12-06	Minor fixes to Arguments	gareuselesinge
2011-11-24	Added a function to inspect current option state.	ppedrot
2011-11-24	Added a DEPRECATED flag in declaration of options. For now only two options a...	ppedrot
2011-11-21	Renamig support added to "Arguments"	gareuselesinge
2011-11-21	New Arguments vernacular	gareuselesinge
2011-11-18	Adding the type infrastructure to handle properly API management of options	ppedrot
2011-11-02	Add type annotations around all calls to Libobject.declare_object	letouzey
2011-10-25	First attempt at making Print Assumption compatible with opaque modules (fix ...	letouzey
2011-10-24	Heads: avoid potentially uncaught Not_found via an assert false	letouzey
2011-10-12	Temporary revert commit 14550 since it breaks a few contribs	letouzey
2011-10-11	in heads.ml, at least turn the Not_found of #2608 into assert false	letouzey
2011-10-11	Various simplifications about constant_of_delta and mind_of_delta	letouzey
2011-10-08	Rely on kernel to know if a name is already used so as to be consistent with it.	herbelin
2011-10-05	Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).	herbelin
2011-09-24	Completing r14448 and thus continuing r14407 (using Cast to propagate	herbelin
2011-09-22	Hash-consing: attempt to stop hash-consing separately constr in declare.ml	letouzey
2011-09-15	Names.make_mbid and co : convert from/to identifier (avoid some String.copy)	letouzey
2011-09-05	Coqide: new backtracking code, based on the Backtrack command	letouzey
2011-09-05	Lib: remove strange code about backtracking to the current state	letouzey
2011-09-05	Lib.node: merge OpenedModtype and OpenedModule, same for Closed...	letouzey
2011-07-29	Heads: generic equality on constr replaced by destructor	puech
2011-05-17	Modops: the strengthening functions can work without any env argument	letouzey
2011-05-11	Print Module (Type) M now tries to print more details	letouzey
2011-04-13	Revert "Add [Polymorphic] flag for defs"	msozeau
2011-04-13	Add [Polymorphic] flag for defs	msozeau
2011-04-03	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey
2011-03-17	Goptions: repair Unset for int options	letouzey
2011-03-05	Added a table for using reserved names for binding names to types	herbelin
2011-02-11	Annotations at functor applications:	letouzey