coq - The formal proof system

Age	Commit message (Expand)	Author
2014-05-06	Cleanup before merge with the trunk	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
2014-03-02	Migrate back g_obligations in toplevel	Pierre Letouzey
2014-02-16	Removing non-marshallable data from the Agram constructor. Instead of	Pierre-Marie Pédrot
2013-12-04	Vernac classification: allow for commands which start proofs but must be sync...	Arnaud Spiwack
2013-08-08	Vernac classification streamlined (handles VERNAC EXTEND)	gareuselesinge
2013-06-06	Uniformizing generic argument types.	ppedrot
2013-04-15	More functional implementation of locality_flag and program_mode	gareuselesinge
2013-03-14	Pptactic.pr_raw_tactic is now without env argument	letouzey
2012-10-16	Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp	letouzey
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-08-08	Updating headers.	herbelin
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-06-01	Getting rid of Pp.msgnl and Pp.message.	ppedrot
2012-05-29	place all files specific to camlp4 syntax extensions in grammar/	letouzey
2012-05-29	Basic stuff about constr_expr migrated from topconstr to constrexpr_ops	letouzey
2012-05-29	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey
2012-05-29	Vernacexpr is now a mli-only file, locality stuff now in locality.ml	letouzey
2012-04-26	migrate g_obligations.ml4 in parsing	letouzey