coq - The formal proof system

Age	Commit message (Expand)	Author
2012-03-02	"Let in" in pattern hell, one more iteration	pboutill
2012-03-02	Noise for nothing	pboutill
2012-02-29	Fix compilation of Constrintern...	pboutill
2012-02-29	RefMan update about match syntax.	pboutill
2012-02-29	In the syntax of pattern matching, the arguments of the inductive in the "in"	pboutill
2012-02-29	In the syntax of pattern matching, "in" clauses are patterns.	pboutill
2012-02-01	Debugger vs tracer: Two different behaviors wrt printing: The debugger	herbelin
2012-01-27	Printing bugs with match patterns:	herbelin
2012-01-20	Added documentation for "Set Parsing Explicit" + fixed mistakenly	herbelin
2012-01-20	Added new command "Set Parsing Explicit" for deactivating parsing (and	herbelin
2012-01-20	Notations with binders: Accepting using notations for functional terms	herbelin
2012-01-19	Boolean Option Patterns Compatibility	pboutill
2012-01-16	Parameters in pattern first step.	pboutill
2012-01-05	Backtracking on r14876 (fix for bug #2267): extra scopes might be	herbelin
2012-01-04	Fixing Arguments Scope bug when too many scopes are given (bug #2667).	herbelin
2011-12-18	Fixing bug #2634 (unscoped notations were disturbing the	herbelin
2011-12-17	A pass on warning printings. Made systematic the use of msg_warning so	herbelin
2011-12-16	Fixing amazing loop when using eta-expansion in pattern-matching for	herbelin
2011-11-21	Renamig support added to "Arguments"	gareuselesinge
2011-11-21	New Arguments vernacular	gareuselesinge
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