coq - The formal proof system

Age	Commit message (Expand)	Author
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
2010-06-06	Added support for Ltac-matching terms with variables bound in the pattern	herbelin
2010-06-06	Updated performance analysis file	herbelin
2010-06-04	Extraction: attempt to provide nice extraction of chars and strings for Ocaml	letouzey
2010-06-04	Ascii: simplier ascii_of_pos, conversion from/to N, proofs about nat-->ascii-...	letouzey
2010-06-04	Extraction: finish ExtrOcamlNatInt, add similar translation nat==>big_int	letouzey
2010-06-04	doc Nstaz updated	pottier
2010-06-04	Backported r13068 to branch v8.3 (whd_betaiota on inferred return	herbelin
2010-06-04	A new command Compute foo, shortcut for Eval vm_compute in foo	letouzey
2010-06-04	Grobner.v removed	pottier
2010-06-03	"Improved" the form of the inferred type of "match" by	herbelin
2010-06-03	Added command "Locate Ltac qid".	herbelin
2010-06-03	Avoid computing tactic printing tree (std_ppcmds) when printing not needed in	herbelin
2010-06-03	plugins/xml: kill two warnings	letouzey
2010-06-03	Ocamlbuild: try to speed-up error detection in .ml, by byte-compiling first	letouzey
2010-06-03	Ide_blob: avoid direct use of Stdpp for compatibility with new camlp4	letouzey
2010-06-03	Misc fixes related to new nsatz (and ocamlbuild)	letouzey
2010-06-03	Add unix.cma on camlp4 command-line in coq_makefile (Closes: #2326)	glondu
2010-06-03	nsatz ajoute	pottier
2010-06-03	ajout oublie	pottier
2010-06-03	plugin groebner updated and renamed as nsatz; first version of the doc of nsa...	pottier
2010-06-02	Fix xml test in non-local mode	glondu