coq - The formal proof system

Age	Commit message (Expand)	Author
2012-01-27	Printing bugs with match patterns:	herbelin
2012-01-20	Added new command "Set Parsing Explicit" for deactivating parsing (and	herbelin
2012-01-19	Boolean Option Patterns Compatibility	pboutill
2012-01-16	Parameters in pattern first step.	pboutill
2011-11-07	Allow "\|_=>_" in "match" in patterns, no more forced enumeration of constructors	letouzey
2011-10-28	Remove dynamic stuff from constr_expr and glob_constr	glondu
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-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-06-12	Rather quick hack to avoid using notations involving "Type" when	herbelin
2011-04-24	Yet another bug in printing fix with let-in binders	herbelin
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
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-10-03	Added multiple implicit arguments rules per name.	herbelin
2010-09-28	Fix function applications without labels (OCaml warning 6)	glondu
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-07-22	Extension of the recursive notations mechanism	herbelin
2010-07-22	Constrintern: unified push_name_env and push_loc_name_env; made	herbelin
2010-06-14	Added printing of recursive notations in cases pattern (supported by wish 2248).	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-18	Fixed some printing bugs.	herbelin
2010-04-10	Optimized need for delimiters when disjoint scopes for strings and	herbelin
2010-01-06	Allowed handling of partly-applied record constructors. (Fix for bug #2196.)	gmelquio
2009-12-13	Deactivating printing of {\| \|} for records when option Printing All is set.	herbelin
2009-11-11	Improving abbreviations/notations + backtrack of semantic change in r12439	herbelin
2009-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin
2009-11-04	Fixed record syntax "{\|x=...; y=...\|}" so that it works with qualified names.	gmelquio
2009-10-29	Revision 12439 continued, printing part (notations to names behave	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-04-08	Some dead code removal + cleanups	letouzey
2009-03-28	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau
2009-02-06	Fixing #2044 (bad printing of primitive notation at the head of	herbelin
2008-11-05	Move Record desugaring to constrintern and add ability to use notations	msozeau
2008-10-23	Open notation for declaring record instances.	msozeau
2008-10-22	Affichage des notations récursives:	herbelin
2008-10-08	Améliorations de l'affichage des coercions suggérées par Georges :	herbelin
2008-07-17	Uniformisation du format des messages d'erreur (commencent par une	herbelin
2008-05-30	Improvements on coqdoc by adding more information into .glob	msozeau
2008-05-06	Postpone the search for the recursive argument index from the user given	msozeau
2008-04-14	Diverses corrections	herbelin
2008-04-13	Bugs, nettoyage, et améliorations diverses	herbelin
2008-03-30	Ajout d'abbréviations/notations paramétriques	herbelin
2008-03-28	- Second pass on implementation of let pattern. Parse "let ' par [as x]?	msozeau
2008-01-17	Add new LetPattern construct to replace dest. syntax: let\| pat := t in b is b...	msozeau