coq - The formal proof system

Age	Commit message (Expand)	Author
2014-12-16	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot
2014-12-11	handling Functional Scheme for required but not imported modules	Julien Forest
2014-10-25	This commit introduces changes in induction and destruct.	Hugo Herbelin
2014-10-13	library/opaqueTables: enable their use in interactive mode	Enrico Tassi
2014-09-22	Fixing bug 3951	Julien Forest
2014-09-17	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau
2014-09-12	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin
2014-09-12	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin
2014-08-05	Experimentally adding an option for automatically erasing an	Hugo Herbelin
2014-08-02	Better struture for Ltac internalization environments in Constrintern.	Pierre-Marie Pédrot
2014-07-29	Add a type of untyped term to Ltac's value.	Arnaud Spiwack
2014-06-08	Moving hook code from Future to Lemmas. This seemed to disrupt compilation of	Pierre-Marie Pédrot
2014-06-08	Enforce a correct exception handling in declaration_hooks	Enrico Tassi
2014-05-08	Renaming new_induct -> induction; new_destruct -> destruct.	Hugo Herbelin
2014-05-06	Adapt universe polymorphic branch to new handling of futures for delayed proofs.	Matthieu Sozeau
2014-05-06	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau
2014-05-06	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2013-12-17	Removing the need of evarmaps in constr internalization.	Pierre-Marie Pédrot
2013-11-25	Remove the Hiddentac module.	Arnaud Spiwack
2013-11-02	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack
2013-10-23	cList.index is now cList.index_f, same for index0	letouzey
2013-10-18	declaration_hooks use Ephemeron	gareuselesinge
2013-09-27	Removing a bunch of generic equalities.	ppedrot
2013-09-02	Removing more association lists in Constrintern.	ppedrot
2013-08-08	get rid of closures in global/proof state	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-05-09	A uniformization step around understand_* and interp_* functions.	herbelin
2013-04-23	Indfun : use States.with_state_protection instead of freeze/unfreeze	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 9)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 7)	letouzey
2013-03-11	Allowing (Co)Fixpoint to be defined local and Let-style.	ppedrot
2013-02-26	kernel/declarations becomes a pure mli	letouzey
2013-02-19	Dir_path --> DirPath	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
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
2012-11-17	Taking into account the type of a definition (if it exists), and the	herbelin
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-09-17	More cleaning on Utils and CList. Some parts of the code being	ppedrot
2012-09-14	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot
2012-09-14	This patch removes unused "open" (automatically generated from	regisgia
2012-09-14	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot