coq - The formal proof system

Age	Commit message (Expand)	Author
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
2011-07-15	A correct error message for an unknown field in a record definition	pboutill
2011-07-11	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-08	Coqide: undo comments (Second part of r14268)	pboutill
2011-07-07	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-06	Fixed bullets so that they would play well with { }.	aspiwack
2011-07-05	Adding a new syntax for BeginSubproof and EndSubproof, namely { and }.	courtieu
2011-07-04	Set Extraction KeepSingleton: an option for not decapsulating singleton types	letouzey
2011-07-04	StrictOrder marked explicitly to be in Prop	letouzey
2011-07-04	Extraction: in haskell, __ may have any type, no need to unsafeCoerce it	letouzey
2011-07-04	Extraction: in haskell, type signatures for __ and unsafeCoerce (fix #2552)	letouzey
2011-07-04	Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml	letouzey
2011-07-04	doc/stdlib: Update the list of ZArith files	letouzey
2011-07-01	Some cleanup of Zcomplements	letouzey
2011-07-01	Cleanup of files related with power over Z.	letouzey