coq - The formal proof system

Age	Commit message (Expand)	Author
2011-11-16	Fixing association of wrong "as"-pattern name when expanding	herbelin
2011-11-07	Allow "\|_=>_" in "match" in patterns, no more forced enumeration of constructors	letouzey
2011-11-02	Add type annotations around all calls to Libobject.declare_object	letouzey
2011-10-29	Fixed broken globalization of identifiers containing utf8 letters	herbelin
2011-10-29	Added checksums to glob files and warned about possibly missing	herbelin
2011-10-28	Remove dynamic stuff from constr_expr and glob_constr	glondu
2011-10-24	Fixing failing printer when the type of a binder name with implicit	herbelin
2011-08-30	Quick improvement of some error messages related to module application	herbelin
2011-08-10	Fixing printing bug with last trailing non-maximally implicit	herbelin
2011-07-26	Partial revert of r14292	pboutill
2011-07-22	Add a syntax entry for fully applied constructor pattern	pboutill
2011-07-22	Internalization of pattern carries a full intern_env	pboutill
2011-07-16	This adds two option tables 'Printing Record' and 'Printing Constructor'	herbelin
2011-07-16	This option disables the use of the '{\| field := ... \|}' notation	herbelin
2011-07-16	Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...	herbelin
2011-07-15	A correct error message for an unknown field in a record definition	pboutill
2011-06-12	Rather quick hack to avoid using notations involving "Type" when	herbelin
2011-06-08	Make Notation works with anonymous-level "Type".	herbelin
2011-05-26	Partial fix for accepting bound variables with same name as implicit	herbelin
2011-05-26	Fixing discriminate for identity.	herbelin
2011-05-05	Definitions of positive, N, Z moved in Numbers/BinNums.v	letouzey
2011-04-25	Fixing and completing interpretation of let's in notations for iterated binders.	herbelin
2011-04-24	Yet another bug in printing fix with let-in binders	herbelin
2011-04-15	Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".	herbelin
2011-04-13	- Remove create_evar_defs	msozeau
2011-04-08	Fixing multiple printing bugs with "Notation f x := ..."	herbelin
2011-03-31	Did that adding a rule for printing applications as "f(x)" works.	herbelin
2011-03-05	Added a table for using reserved names for binding names to types	herbelin
2011-03-05	Moving printing of module typing errors upwards to himsg.ml so as to	herbelin
2011-02-12	fix last commit about modules (subst_cl_typ may raise Not_found)	letouzey
2011-02-11	An automatic substitution of scope at functor application	letouzey
2011-02-11	Annotations at functor applications:	letouzey
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	local variables can have implicits locally	pboutill
2011-02-10	Data structure telling implicits of local variables is a map in the	pboutill
2011-02-10	internalize now use a record for its env	pboutill
2011-02-10	More comments and less doublons in some mli	pboutill
2011-01-31	Coqlib.gen_constant_in_modules can take a qualid string "Foo.bar"	letouzey
2011-01-31	A fine-grain control of inlining at functor application via priority levels	letouzey
2010-12-25	Rename mkR* smart constructors (mostly in funind)	glondu
2010-12-24	More {raw => glob} changes for consistency	glondu
2010-12-23	Fix diagram in genarg.mli	glondu
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-12-23	Change of nomenclature: rawconstr -> glob_constr	glondu
2010-12-23	Prepare change of nomenclature rawconstr -> glob_constr	glondu
2010-12-04	Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).	herbelin
2010-12-04	Fixing several bugs with links to notation in coqdoc, including bug #2445:	herbelin
2010-11-07	Add information of localisation when an error involving an "implicit	herbelin
2010-11-04	Fixing a regression wrt 8.2 when using an "ident" several times in a notation	herbelin