coq - The formal proof system

Age	Commit message (Expand)	Author
2010-06-14	Fixed commit 13125 (stricter check of induction args): an interpretation	herbelin
2010-06-14	Alert on the possible incompatibilties with set_add (see bug 2111) which	herbelin
2010-06-14	Extraction Implicit: documentation	letouzey
2010-06-14	Added printing of recursive notations in cases pattern (supported by wish 2248).	herbelin
2010-06-13	Fixing bug 2295 (omission of option "as" in return clause of "match" was not	herbelin
2010-06-13	Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).	herbelin
2010-06-13	Addressed bug #2320 in v8.2 and v8.3 branches ("refine" problem with	herbelin
2010-06-13	Fixing definition of set_map (bug report #2111) which was actually already	herbelin
2010-06-13	Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"	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	Added regression tests for bugs + miscellaneous improvements	herbelin
2010-06-12	Applying François' patch fixing grammar of uniform inheritance condition mes...	herbelin
2010-06-12	Fixing spelling: pr_coma -> pr_comma	herbelin
2010-06-12	Improved the inference of the return predicate in dependent pattern-matching.	herbelin
2010-06-12	Added rudimentary support for using constructors from the explicit	herbelin
2010-06-12	Fixed a bug in evarutil.ml (wrong env of a postponed conversion problem).	herbelin
2010-06-12	Added debugging printer for the idmap used at evar definition time for	herbelin
2010-06-11	Reverted commit 13110 about headers.sty that I wrongly thought was buggy. Sorry.	herbelin
2010-06-11	Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).	herbelin
2010-06-10	Fixed two bugs in pattern-matching compilation	herbelin
2010-06-10	Fixed a very old (from V6.3) typo in headers.sty	herbelin
2010-06-10	Extraction Implicits: can accept argument names instead of just positions	letouzey
2010-06-10	Fix build with OCaml 3.12	glondu
2010-06-09	Fixed bug # 2303 in r 13087.	msozeau
2010-06-09	Tentative fix for bug #2226: put inj_pair2 and eq_dep_eq hints in a	msozeau
2010-06-09	Fix bug #2317: setoid_rewrite ignored binding lists. Slightly	msozeau
2010-06-09	Fix bug #2262: bad implicit argument number by avoiding counting	msozeau
2010-06-09	Keep description of Automatic Introduction at only one place of CHANGES.	herbelin
2010-06-09	Relaxed the freshness constraint in "intro H" (with "H" explicit):	herbelin
2010-06-09	Allowing to use an ordering different than Lt with measure	jforest
2010-06-09	Automatic introduction of names given before ":" in Lemma's and	herbelin
2010-06-09	Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.	herbelin
2010-06-08	Fixing commit r13090 (forgot to commit the file generating Nmake_gen.v).	herbelin
2010-06-08	Using vernac parsing for Function	jforest
2010-06-08	Extraction with implicits: perform the occur-check after optimisations	letouzey
2010-06-08	Fixed wrong spelling in a warning.	herbelin
2010-06-08	Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".	herbelin
2010-06-08	Made option "Automatic Introduction" active by default before too many	herbelin
2010-06-08	Typo in ExtrOcamlString: list char instead of char list	letouzey
2010-06-08	Fix unfolding tactic for well-founded Programs.	msozeau
2010-06-08	Tentative fix for typeclass resolution raising Evd.define exceptions.	msozeau
2010-06-08	Fix treatment of {struct x} annotations in presence of generalized	msozeau
2010-06-07	Fix comment	glondu
2010-06-07	Document grammar.cma->unix.cma dependency in CHANGES	glondu
2010-06-07	Replace ld by gcc in ocamlopt_shared_os5fix.sh (Closes: #2325)	glondu
2010-06-07	fixing error message display.	vgross
2010-06-07	Backporting part of r12970 to trunk (deprecation of double induction).	herbelin