coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Centralizing the Ltac-defining functions in Tacenv.	ppedrot	2013-11-10
*	Made multiple-goal tactic work after all: .	aspiwack	2013-11-02
*	Fixes parsing of all: followed by a typechecking/evaluation command.	aspiwack	2013-11-02
*	Adds a new goal selector "all:".	aspiwack	2013-11-02
*	The tactic [admit] exits with the "unsafe" status.	aspiwack	2013-11-02
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	Conv_orable made functional and part of pre_env	gareuselesinge	2013-10-31
*	cList: a few alternative to hashtbl-based uniquize, distinct, subset	letouzey	2013-10-23
*	cList: set-as-list functions are now with an explicit comparison	letouzey	2013-10-23
*	declaration_hooks use Ephemeron	gareuselesinge	2013-10-18
*	Remove some uses of local modules (some were unused, some were costly).	xclerc	2013-10-14
*	STM: fix verbosity of queries	gareuselesinge	2013-10-07
*	Moving side effects into evar_map. There was no reason to keep another	ppedrot	2013-10-05
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	get rid of closures in global/proof state	gareuselesinge	2013-08-08
*	Support Proof General	gareuselesinge	2013-08-08
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Replacing uses of association lists by maps in notations.	ppedrot	2013-08-03
*	Added a Print Debug GC command that displays the current state of	ppedrot	2013-08-01
*	Granting bug #3098: adding priority to Existing Instances.	ppedrot	2013-08-01
*	better error message for unexpected renaming (closes #2987)	gareuselesinge	2013-07-29
*	Revert "Only arguments declared as implicit can be renamed"	gareuselesinge	2013-07-29
*	Declaremods: major refactoring, stop duplicating libobjects in modules	letouzey	2013-07-17
*	Added a Register Inline command for the native compiler. Will be ported to th...	mdenes	2013-07-10
*	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot	2013-06-21
*	Fixing bug #3030.	ppedrot	2013-06-06
*	Replacing Id.check with Id.is_valid, as its sole use was under	ppedrot	2013-05-14
*	A uniformization step around understand_* and interp_* functions.	herbelin	2013-05-09
*	Declaration of multiple hypotheses or parameters now share typing	herbelin	2013-05-08
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	raise UnsafeSuccess -> feedback AddedAxiom	gareuselesinge	2013-04-25
*	Fix issues with "Reset Initial" in scripts given to coqtop -l	letouzey	2013-04-23
*	Only arguments declared as implicit can be renamed	gareuselesinge	2013-04-18
*	More functional implementation of locality_flag and program_mode	gareuselesinge	2013-04-15
*	Moved the Loadpath part of Library to its own file, and documented	ppedrot	2013-03-26
*	Check unexpected "Local" keyword in cmd before opening a proof (fix #2975)	letouzey	2013-03-21
*	Removing the module Libtypes and unifying the Search[Pattern\|Rewrite]?	ppedrot	2013-03-19
*	Avoid a few overzealous "when Errors.noncritical"	letouzey	2013-03-17
*	Restrict (try...with...) to avoid catching critical exn (part 13)	letouzey	2013-03-13
*	Allowing (Co)Fixpoint to be defined local and Let-style.	ppedrot	2013-03-11
*	Added a Local Definition vernacular command. This type of definition	ppedrot	2013-03-11
*	Update debug code according to reorganization into modules.	msozeau	2013-02-27
*	avoid (Int.equal (cmp ...) 0) when a boolean equality exists	letouzey	2013-02-19
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Removing Exc_located and using the new exception enrichement	ppedrot	2013-02-18
*	Minor code cleanups, especially take advantage of Dir_path.is_empty	letouzey	2013-02-18
*	Useless use of hooks in VernacDefinition. In addition, this was	ppedrot	2013-02-10
*	Actually adding backtrace handling.	ppedrot	2013-01-28
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Modulification of name	ppedrot	2012-12-18