coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	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	2011-07-16
*	A correct error message for an unknown field in a record definition	pboutill	2011-07-15
*	Makefiles generated by coq_makefile can build %.cmx?a from %.mllib	pboutill	2011-07-11
*	Stores bullet stack on locally at the level of focuses rather than globally i...	aspiwack	2011-07-11
*	Coqide: undo comments (Second part of r14268)	pboutill	2011-07-08
*	coq_makefile logical path ending with '.' are correctly convert to physical path	pboutill	2011-07-07
*	coq_makefile bug fix 2405: cmxs are now made from cmx files	pboutill	2011-07-07
*	coq_makefile documentation in Refman and -h	pboutill	2011-07-07
*	coq_makefile doesn't complain anymore when a dir is both -I and -R	pboutill	2011-07-07
*	Bug 2217: In coqide, a comment alone is now a sentence that isn't send to coq	pboutill	2011-07-07
*	Coqide understand { and }	pboutill	2011-07-07
*	default install location under cygwin is the unix default	pboutill	2011-07-07
*	bug 2423: consider "" as the empty prefix	barras	2011-07-07
*	fixed coqchk usage and man page + added option -coqlib	barras	2011-07-07
*	Fixed bullets so that they would play well with { }.	aspiwack	2011-07-06
*	Adding a new syntax for BeginSubproof and EndSubproof, namely { and }.	courtieu	2011-07-05