coq - The formal proof system

Age	Commit message (Expand)	Author
2011-02-14	- Fix treatment of globality flag for typeclass instance hints (they	msozeau
2011-02-11	An automatic substitution of scope at functor application	letouzey
2011-02-11	Annotations at functor applications:	letouzey
2011-02-10	Remove obsolete TheoryList	glondu
2011-02-10	Fixpoints are traverse during implicits arguments search to toplevel	pboutill
2011-02-10	Interp a definition with the implicit arguments of its local context	pboutill
2011-02-10	Data structure telling implicits of local variables is a map in the	pboutill
2011-02-10	More comments and less doublons in some mli	pboutill
2011-02-10	Started to fix the declarative proof mode (C-zar).	aspiwack
2011-01-31	A fine-grain control of inlining at functor application via priority levels	letouzey
2011-01-28	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey
2011-01-11	Add "Print Sorted Universes"	glondu
2011-01-11	Use dashed lines for equivalence edges in dot output of universes	glondu
2011-01-06	Reverted r13715 "Add improved indenters that rely on the current proof state ...	gmelquio
2011-01-06	Remove Safe_marshal	glondu
2010-12-24	More {raw => glob} changes for consistency	glondu
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-12-23	Change of nomenclature: rawconstr -> glob_constr	glondu
2010-12-15	Misc improvements about evar_map	letouzey
2010-12-14	Add improved indenters that rely on the current proof state to choose the ind...	gmelquio
2010-12-10	First release of Vector library.	pboutill
2010-12-03	Fixing bug using explictly declared implicit arguments in inductive arities.	herbelin
2010-12-03	Redirect stdout to stderr in -ideslave	glondu
2010-12-02	Fixing a bug introduced in r12304 (move of interpretation of	herbelin
2010-11-18	Do not throw an error for anonymous generalized binders as they will be	msozeau
2010-11-16	Remove redundant clause (and fix compatibility issue)	glondu
2010-11-15	Minor fixes from Gregory Malecha. A typo fixed and a better (located)	msozeau
2010-11-07	Delayed the evar normalization in error messages to the last minute	herbelin
2010-11-07	Add information of localisation when an error involving an "implicit	herbelin
2010-11-07	correcting a non catch error reported as an anomaly (Ploc.Exc)	jforest
2010-11-03	In Univ, unify order_request and constraint_type	glondu
2010-11-02	Output universe graph in DOT language if output file ends in .dot or .gv	glondu
2010-11-02	More generic Univ.dump_universes	glondu
2010-11-02	Move stuff about positive into a distinct PArith subdir	letouzey
2010-11-01	Restored checking that _all_ arguments of the command line are meaningful	herbelin
2010-10-31	Add tolerance for existential variables in Check.	herbelin
2010-10-31	Minor code improvements around libobject	herbelin
2010-10-31	Minor factorization of the part of the code used for Unnamed_thm saving.	herbelin
2010-10-26	Compatibility camlp4/camlp5	herbelin
2010-10-26	Fail, when successful, prints something only in verbose mode	glondu
2010-10-23	Fixing bug #2412, continued (preprocessing of Ltac Debug errors	herbelin
2010-10-23	Fixing bug #2412 (preprocessing of Ltac Debug errors forgotten in r13431).	herbelin
2010-10-17	About "unsupported" unicode characters in notations.	herbelin
2010-10-11	Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, looping	herbelin
2010-10-07	Fix bug# 2392	msozeau
2010-10-06	Remove Explain* vernacs	glondu
2010-10-06	Remove VernacGo	glondu
2010-10-04	Two [Evd.fold] turned into [Evd.fold_undefined].	aspiwack
2010-10-03	Avoid raising an anomaly when an error encapsulated with a dummy	herbelin
2010-10-03	Added multiple implicit arguments rules per name.	herbelin