coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Remove kind_of_type, kind_of_term2 (dead code)	glondu	2010-09-28
*	Fix bug in implementation of setoid rewriting under cases and	msozeau	2010-09-27
*	Fixed a bug in printing fix/cofix error messages when several	herbelin	2010-09-24
*	Solving bug #2212 (unification under tuples now not allowed for	herbelin	2010-09-24
*	Partial review of removed dead code (r13460)	herbelin	2010-09-24
*	Checker: remove some dead code	letouzey	2010-09-24
*	Dead code in extraction	letouzey	2010-09-24
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	dev/Makefile.oug: how to run the Oug analyser, for instance for finding dead ...	letouzey	2010-09-24
*	Added a section in the documentation of Vernacular commands about Set/Unset/T...	aspiwack	2010-09-23
*	Update CHANGES: Local/Global Set/Unset.	aspiwack	2010-09-23
*	Fix inconsistency in Prop/Set conversion check	glondu	2010-09-23
*	Report fix bug 2345 from v8.3 (Bad error message when functional	courtieu	2010-09-21
*	Added eta-expansion in kernel, type inference and tactic unification,	herbelin	2010-09-20
*	Fixed test of bug #2360 (use of Fail to check a regular error instead	herbelin	2010-09-20
*	Extraction: re-introduce some eta-expansions in rare situations leading to '_...	letouzey	2010-09-20
*	Fixing bug #2389 (keyword "Declare Instance" unknown from "coqdoc -g") but	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
*	Hopefully a fix for #2176 (redirection not understood with some shells)	herbelin	2010-09-19