coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Zeven: some complements, e.g. proofs that Zeven_bool and co are ok	letouzey	2010-10-14
*	NArith: add some functions Neven and Nodd	letouzey	2010-10-14
*	NArith: Definition of a Npow power function	letouzey	2010-10-14
*	Ring : Cpow in Type rather than Set (type of power coeffs in power_theory)	letouzey	2010-10-14
*	Adding test-case for bug #2362, which uses HO unification during	msozeau	2010-10-12
*	Fix bug #2393: allow let-ins inside telescopes (only fails when there's	msozeau	2010-10-12
*	Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, looping	herbelin	2010-10-11
*	More precise description of boolean ring in doc (see bug #2401)	glondu	2010-10-11
*	Export the "bullet" grammar entry	glondu	2010-10-08
*	update CHANGES w.r.t. extraction	letouzey	2010-10-08
*	Fix bug# 2392	msozeau	2010-10-07
*	TeX input method is now supported upstream	vgross	2010-10-07
*	test-suite: fix success/unification.v	glondu	2010-10-07
*	Fixing the Not_found error in bug #2404 + dead code removal in cases.ml	herbelin	2010-10-06
*	Remove Explain* vernacs	glondu	2010-10-06
*	Extraction: allow to use Extraction Inline / NoInline even from under a section.	letouzey	2010-10-06
*	test-suite: fix output/Existentials.out	glondu	2010-10-06
*	Remove ide/coq_tactics.ml*	glondu	2010-10-06
*	Remove VernacGo	glondu	2010-10-06
*	Remove unused unshare_proof_tree from xml plugin	glondu	2010-10-06
*	Remove open_subgoals field of proof_tree	glondu	2010-10-06
*	(Hopefully) clearer explanation of Ltac's context patterns	glondu	2010-10-05
*	test-suite: fix success/Typeclasses.v	glondu	2010-10-05
*	test-suite: fix success/AdvancedCanonicalStructure.v	glondu	2010-10-05
*	Export definition of type implicits_list for contribs + fixed a	herbelin	2010-10-05
*	Reintroduce kind_of_type (used by Presburger contrib)	glondu	2010-10-05
*	Auto-inlining of f_terminate in Function	jforest	2010-10-05
*	test-suite: use unified diff output and use expected output as reference	glondu	2010-10-05
*	Forgotten lifts in eta-expansion	glondu	2010-10-04
*	Install a printer for fconstr (ppconstr was installed twice)	glondu	2010-10-04
*	Two [Evd.fold] turned into [Evd.fold_undefined].	aspiwack	2010-10-04
*	Fixing bugs in previous commits about implicit arguments:	herbelin	2010-10-04
*	Avoid raising an anomaly when an error encapsulated with a dummy	herbelin	2010-10-03
*	Test for non-regression of the display bug fixed in r13486.	herbelin	2010-10-03
*	Fixing printing of module_path names (was using a debugging	herbelin	2010-10-03
*	Using multiple lists of implicit arguments in Program for preserving	herbelin	2010-10-03
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Dead code in impargs (afaics, no more need, since r11242, to merge	herbelin	2010-10-03
*	Making display of various informations about constants more modular:	herbelin	2010-10-03
*	Fixed a little printing bug with "About" on an undefined constant.	herbelin	2010-10-03
*	Simplify tactic(_)-bound arguments in TACTIC EXTEND rules	glondu	2010-09-30
*	Improve handling of metas as evars in unification (patch by Hugo)	letouzey	2010-09-30
*	Speed-up refine by avoiding some calls to Evd.fold	letouzey	2010-09-30
*	Fix bug #2321, allowing "_" named projections in classes. Not realizing	msozeau	2010-09-28
*	Coqdoc patches from UPenn (thanks to C. Casinghino). This introduces the	msozeau	2010-09-28
*	Minor fixes of 'make doc'	pboutill	2010-09-28
*	Bvector.Vshiftin was wrong for ages	pboutill	2010-09-28
*	Remove some occurrences of "open Termops"	glondu	2010-09-28
*	Fix function applications without labels (OCaml warning 6)	glondu	2010-09-28
*	Remove "init" label from Termops.it_mk* specialized functions	glondu	2010-09-28