coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Sequent: generic equality on constr replaced by destructors	puech	2011-07-29
*	Sequent: generic equality on ident replaced by id_ord	puech	2011-07-29
*	Instances: generic equality on global_reference replaced by RefOrdered.compare	puech	2011-07-29
*	Unify: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Eqschemes: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Evarutil: generic equality on constr replaced by destructors	puech	2011-07-29
*	Heads: generic equality on constr replaced by destructor	puech	2011-07-29
*	Environ: generic equality on named_context replaced by named_context_equal	puech	2011-07-29
*	Evarconv: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Equality: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Cases: generic equality on constr replaced by destructors	puech	2011-07-29
*	Tactics: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Classops: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Class: generic equality on constr replaced by destructors	puech	2011-07-29
*	Evarutil: generic equality on constr replaced by eq_constr (x2)	puech	2011-07-29
*	Equality: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Tactics: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Tactics: generic equality on named_declaration replaced by eq_named_declaration	puech	2011-07-29
*	Term: added function eq_named_declaration	puech	2011-07-29
*	Evarutil: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Tacred: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Hipattern: two generic equalities on constr spotted & rewritten	puech	2011-07-29
*	Indtypes: remove useless and wrong generic equality test on constr array	puech	2011-07-29
*	Term: slight reorganization of the file	puech	2011-07-29
*	Term_typing, Typeops: replace some generic '=' on constr by eq_constr	puech	2011-07-29
*	Term: Refactoring of hashconsing	puech	2011-07-29
*	argument renaming in liftn (match with usual terminology)	puech	2011-07-29
*	Ide_slave: same attributes for { } and Focus/Unfocus (fix coqide display)	letouzey	2011-07-28
*	Coqide: GEdit.combo is deprecated since Gtk2.4! We now use GEdit.combo_box_en...	pboutill	2011-07-27
*	Oversight in revision 14292.	pboutill	2011-07-27
*	Typo of bug 2577	pboutill	2011-07-27
*	or_introl is now too complicated for basic tests of test-suite/output/PrintIn...	pboutill	2011-07-26
*	Partial revert of r14292	pboutill	2011-07-26
*	ide/coq_lex.mll: restore the separate parsing of .. (fix #2578)	letouzey	2011-07-26
*	Integral domains	pottier	2011-07-26
*	Ring2 devient Ncring et la reification par les type classes est partagee	pottier	2011-07-26
*	All the parameters of Compare are implicits.	pboutill	2011-07-26
*	All the parameters of or can be implicits.	pboutill	2011-07-26
*	Same Implicit Arguments rule for sumbool and sumor.	pboutill	2011-07-26
*	Coqide: fixes and clarifications concerning sentence-terminators	letouzey	2011-07-25
*	Add a syntax entry for fully applied constructor pattern	pboutill	2011-07-22
*	Internalization of pattern carries a full intern_env	pboutill	2011-07-22
*	Allow custom targets without commands specified	pboutill	2011-07-22
*	For the beauty of tail recursion, a new list_addn	pboutill	2011-07-22
*	Fix typo in coqmktop help	glondu	2011-07-20
*	Fixed a "feature" of "inversion" and "dependent rewrite" revealed by	herbelin	2011-07-18
*	This adds two option tables 'Printing Record' and 'Printing Constructor'	herbelin	2011-07-16
*	This is exactly the structure needed to handle controlling printing	herbelin	2011-07-16
*	This option disables the use of the '{\| field := ... \|}' notation	herbelin	2011-07-16
*	Some facts about functional extensionality (especially alternative	herbelin	2011-07-16