coq - The formal proof system

Age	Commit message (Expand)	Author
2013-11-02	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack
2013-10-24	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-23	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-18	declaration_hooks use Ephemeron	gareuselesinge
2013-09-27	Removing a bunch of generic equalities.	ppedrot
2013-09-19	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc
2013-09-02	Removing more association lists in Constrintern.	ppedrot
2013-08-30	recdef: restore old semantics (pre STM)	gareuselesinge
2013-08-30	Fix typo in error message	gareuselesinge
2013-08-22	Nicer code concerning dirpaths and modpath around Lib	letouzey
2013-08-22	Less "Coq" strings everywhere	letouzey
2013-08-08	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-03	Replacing uses of association lists by maps in notations.	ppedrot
2013-06-25	Useless use of maps in constr internalizing.	ppedrot
2013-06-22	Generalizing the use of maps instead of lists in the interpretation	ppedrot
2013-06-21	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot
2013-06-06	Uniformizing generic argument types.	ppedrot
2013-05-09	Use definition_entry to declare local definitions	gareuselesinge
2013-05-09	A uniformization step around understand_* and interp_* functions.	herbelin
2013-05-06	States: frozen states can hold closures	gareuselesinge
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-04-23	Indfun : use States.with_state_protection instead of freeze/unfreeze	letouzey
2013-04-22	code simplifications concerning Summary	letouzey
2013-04-02	Revised infrastructure for lazy loading of opaque proofs	letouzey
2013-03-13	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-12	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-11	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-02-26	kernel/declarations becomes a pure mli	letouzey
2013-02-19	Dir_path --> DirPath	letouzey
2013-02-18	use List.rev_map whenever possible	letouzey
2013-02-18	Minor code cleanups, especially take advantage of Dir_path.is_empty	letouzey
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2013-01-22	New implementation of the conversion test, using normalization by evaluation to	mdenes
2012-12-18	Modulification of name	ppedrot
2012-12-18	Modulification of Label	ppedrot
2012-12-14	Modulification of dir_path	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-12-14	Moved Intset and Intmap to Int namespace.	ppedrot