coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	I forgot a line in previous commit.	aspiwack	2012-06-22
*	A call to the command Proof (and its variants) now prints the subgoals.	aspiwack	2012-06-22
*	Getting rid of Pcoq remains.	ppedrot	2012-06-12
*	Separated notice vs info messages, and cleaned up the interface a bit.	ppedrot	2012-06-04
*	More cleaning	ppedrot	2012-06-01
*	Cleaning Pp.ppnl use	ppedrot	2012-06-01
*	Getting rid of Pp.msgnl and Pp.message.	ppedrot	2012-06-01
*	Getting rid of Pp.msg	ppedrot	2012-05-30
*	More uniformisation in Pp.warn functions.	ppedrot	2012-05-30
*	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
*	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-05-29
*	Vernacexpr is now a mli-only file, locality stuff now in locality.ml	letouzey	2012-05-29
*	Program: avoid staying in program mode after a failed Program command	letouzey	2012-04-26
*	correct abort in Function when a proof of inversion fails	letouzey	2012-04-23
*	Corrects a (very) longstanding bug of tactics. As is were, tactic expecting	aspiwack	2012-04-18
*	lib directory is cut in 2 cma.	pboutill	2012-04-12
*	Added a command "Unfocused" which returns an error when the proof is	aspiwack	2012-03-30
*	Slight change in the semantics of arguments scopes: scopes can no	herbelin	2012-03-26
*	A unified backtrack mechanism, with a basic "Show Script" as side-effect	letouzey	2012-03-23
*	Remove undocumented command "Delete foo"	letouzey	2012-03-23
*	Remove old proof-managment commands Suspend/Resume	letouzey	2012-03-23
*	Force Check (which, from 8.4beta, accepts unresolved evars) to however	herbelin	2012-03-20
*	Fix bugs related to Program integration.	msozeau	2012-03-19
*	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau	2012-03-14
*	Second step of integration of Program:	msozeau	2012-03-14
*	Noise for nothing	pboutill	2012-03-02
*	Arguments supports extra notation scopes	gareuselesinge	2012-02-14
*	Removed a seemingly unused argument in Require of modules, introduced 10 year...	ppedrot	2012-01-23
*	Added new command "Set Parsing Explicit" for deactivating parsing (and	herbelin	2012-01-20
*	Arguments: check rename even if no implicit is specified	gareuselesinge	2011-12-19
*	Command Arguments: standardizing format of error messages and American spelling.	herbelin	2011-12-17
*	Moving bullets (-, +, *) into stand-alone commands instead of being	courtieu	2011-12-16
*	Proof using ...	gareuselesinge	2011-12-12
*	Minor fixes to Arguments	gareuselesinge	2011-12-06
*	Added a DEPRECATED flag in declaration of options. For now only two options a...	ppedrot	2011-11-24
*	Correct direction for definitional typeclasses	msozeau	2011-11-24
*	Renamig support added to "Arguments"	gareuselesinge	2011-11-21
*	New Arguments vernacular	gareuselesinge	2011-11-21
*	Adding the type infrastructure to handle properly API management of options	ppedrot	2011-11-18
*	Restore backward compatibility. ":>" declares subinstances in Class declarati...	msozeau	2011-11-18
*	Merge subinstances branch by me and Tom Prince.	msozeau	2011-11-17
*	First attempt at making Print Assumption compatible with opaque modules (fix ...	letouzey	2011-10-25
*	Re-allowing assumptions during proofs seems safe now (fix #2411)	letouzey	2011-09-15
*	Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...	aspiwack	2011-09-12
*	Lib.node: merge OpenedModtype and OpenedModule, same for Closed...	letouzey	2011-09-05
*	Remove code concerning the obsolete Set/Unset Undo	letouzey	2011-09-05