coq - The formal proof system

Age	Commit message (Expand)	Author
2014-01-20	bug correction in proving principles of function	jforest
2013-12-24	Qed: feedback when type checking is done	Enrico Tassi
2013-12-17	Removing the need of evarmaps in constr internalization.	Pierre-Marie Pédrot
2013-12-04	Factoring(continued).	Arnaud Spiwack
2013-12-04	Refactoring: storing more information in the terminator closure.	Arnaud Spiwack
2013-12-04	The commands that initiate proofs are now in charge of what happens when proo...	Arnaud Spiwack
2013-12-04	Vernac classification: allow for commands which start proofs but must be sync...	Arnaud Spiwack
2013-11-27	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot
2013-11-25	Remove the Hiddentac module.	Arnaud Spiwack
2013-11-21	Add Acc_intro_generator on top of all wf function proof (much much faster exe...	Julien Forest
2013-11-08	Porting Tactics.assumption to the new engine.	ppedrot
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-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