coq - The formal proof system

Age	Commit message (Expand)	Author
2010-09-28	Remove some occurrences of "open Termops"	glondu
2010-09-28	Remove "init" label from Termops.it_mk* specialized functions	glondu
2010-09-27	Fix bug in implementation of setoid rewriting under cases and	msozeau
2010-09-24	Solving bug #2212 (unification under tuples now not allowed for	herbelin
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-09-20	Added eta-expansion in kernel, type inference and tactic unification,	herbelin
2010-09-19	Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't we	herbelin
2010-09-19	Reverting partial fix for #2335 committed by mistake in r13435. Sorry.	herbelin
2010-09-19	Patch solving the bug but leaving open design choices	herbelin
2010-09-17	Fixed a problem introduced in r12607 after pattern_of_constr served	herbelin
2010-09-17	In the computation of missing arguments for apply, accept that the	herbelin
2010-09-13	Fix unescaped end-of-lines (OCaml warning 29)	glondu
2010-09-11	Improving a few error messages in Ltac interpretation	herbelin
2010-09-02	* removed declare_constant and declare_internal_constant	vsiles
2010-09-02	Improved printing of Unfoldable constants in hints databases (used	herbelin
2010-08-03	Export printing functions for extra arguments. Maybe there's a way to	msozeau
2010-07-30	Capitulation wrt "change pat with term": instead of solving the	herbelin
2010-07-28	Fix bug #2209, don't use the fragile argument name "y" to pass the	msozeau
2010-07-28	oops. commited files I shouldn't have. reverting on r13341	barras
2010-07-28	ported r13340 to trunk	barras
2010-07-27	Minor fixes:	msozeau
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-07-22	Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).	herbelin
2010-07-22	Adding the destauto tactic, that reduces match by destructing matched	courtieu
2010-07-21	Fix for bug #2350 was really too quick. Here is a version that works better.	herbelin
2010-07-21	Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).	herbelin
2010-07-18	Reverted 13293 commited mistakenly. Sorry for the noise.	herbelin
2010-07-18	Tentative de suppression de l'import automatique des hints et coercions.	herbelin
2010-07-15	Be more clever when trying to find out the relation in	msozeau
2010-07-09	Finish adding out-of-the-box support for camlp4	letouzey
2010-06-30	Fix generalize_eqs tactic to not consider defined variables as being generali...	msozeau
2010-06-29	Made tclABSTRACT normalize evars before saying it does not support	herbelin
2010-06-28	Made "replace" accepts open terms on its left-hand-side.	herbelin
2010-06-28	Fixed a bug introduced in a combination in r12807 and revealed in	herbelin
2010-06-22	Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).	herbelin
2010-06-22	New script dev/tools/change-header to automatically update Coq files headers.	herbelin
2010-06-14	Fixed commit 13125 (stricter check of induction args): an interpretation	herbelin
2010-06-13	Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).	herbelin
2010-06-13	Fixed bug #2314 (inversion using not checking the correctness of its arguments	herbelin
2010-06-13	Made intros_until and onInductionArg a bit stricter and robust	herbelin
2010-06-13	Fixed a bug in pretty-printing "induction" and "destruct" due to a	herbelin
2010-06-12	Fixed bug #2135 (second-order unification was raising cryptic message)	herbelin
2010-06-12	Fixing spelling: pr_coma -> pr_comma	herbelin
2010-06-09	Fix bug #2317: setoid_rewrite ignored binding lists. Slightly	msozeau
2010-06-09	Relaxed the freshness constraint in "intro H" (with "H" explicit):	herbelin
2010-06-08	Tentative fix for typeclass resolution raising Evd.define exceptions.	msozeau
2010-06-06	Added support for Ltac-matching terms with variables bound in the pattern	herbelin
2010-06-03	Avoid computing tactic printing tree (std_ppcmds) when printing not needed in	herbelin
2010-05-29	New pass on inductive schemes	herbelin
2010-05-26	Fixing Derive Inversion for new proof engine	herbelin