coq - The formal proof system

Age	Commit message (Expand)	Author
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-28	Ide_slave: same attributes for { } and Focus/Unfocus (fix coqide display)	letouzey
2011-07-27	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-26	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-25	Coqide: fixes and clarifications concerning sentence-terminators	letouzey
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-22	Allow custom targets without commands specified	pboutill
2011-07-22	For the beauty of tail recursion, a new list_addn	pboutill
2011-07-20	Fix typo in coqmktop help	glondu
2011-07-18	Fixed a "feature" of "inversion" and "dependent rewrite" revealed by	herbelin
2011-07-16	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	More lemmas relating the different equivalent formulations of eq_dep.	herbelin
2011-07-16	Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)	herbelin
2011-07-16	Changed name of internally defined "_sym" scheme to avoid confusion with Logi...	herbelin
2011-07-16	Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...	herbelin
2011-07-16	Finally, pr_goal seems to work for printing v8.2 style goal in debugger.	herbelin
2011-07-16	Added a characterization of unique existence.	herbelin