coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Rtree : cleanup of the comparing code	letouzey	2013-10-24
*	Turn many List.assoc into List.assoc_f	letouzey	2013-10-24
*	cList.index is now cList.index_f, same for index0	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
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	Removing more association lists in Constrintern.	ppedrot	2013-09-02
*	recdef: restore old semantics (pre STM)	gareuselesinge	2013-08-30
*	Fix typo in error message	gareuselesinge	2013-08-30
*	Nicer code concerning dirpaths and modpath around Lib	letouzey	2013-08-22
*	Less "Coq" strings everywhere	letouzey	2013-08-22
*	calling interp by hand is forbidden	gareuselesinge	2013-08-08
*	get rid of closures in global/proof state	gareuselesinge	2013-08-08
*	Vernac classification streamlined (handles VERNAC EXTEND)	gareuselesinge	2013-08-08
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Replacing uses of association lists by maps in notations.	ppedrot	2013-08-03
*	Useless use of maps in constr internalizing.	ppedrot	2013-06-25
*	Generalizing the use of maps instead of lists in the interpretation	ppedrot	2013-06-22
*	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot	2013-06-21
*	Uniformizing generic argument types.	ppedrot	2013-06-06
*	Use definition_entry to declare local definitions	gareuselesinge	2013-05-09
*	A uniformization step around understand_* and interp_* functions.	herbelin	2013-05-09
*	States: frozen states can hold closures	gareuselesinge	2013-05-06
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Indfun : use States.with_state_protection instead of freeze/unfreeze	letouzey	2013-04-23
*	code simplifications concerning Summary	letouzey	2013-04-22
*	Revised infrastructure for lazy loading of opaque proofs	letouzey	2013-04-02
*	Restrict (try...with...) to avoid catching critical exn (part 15)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 11)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 9)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 7)	letouzey	2013-03-13
*	Recdef: an anomaly isn't so anomalous, occurs in 1618.v	letouzey	2013-03-12
*	invalid_arg instead of raise (Invalid_argement ...)	letouzey	2013-03-12
*	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
*	kernel/declarations becomes a pure mli	letouzey	2013-02-26
*	Dir_path --> DirPath	letouzey	2013-02-19
*	use List.rev_map whenever possible	letouzey	2013-02-18
*	Minor code cleanups, especially take advantage of Dir_path.is_empty	letouzey	2013-02-18
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of Label	ppedrot	2012-12-18
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Moved Intset and Intmap to Int namespace.	ppedrot	2012-12-14