coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Extraction: allow to use Extraction Inline / NoInline even from under a section.	letouzey	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
*	Auto-inlining of f_terminate in Function	jforest	2010-10-05
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Simplify tactic(_)-bound arguments in TACTIC EXTEND rules	glondu	2010-09-30
*	Fix bug #2321, allowing "_" named projections in classes. Not realizing	msozeau	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-28
*	Dead code in extraction	letouzey	2010-09-24
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	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
*	Extraction: re-introduce some eta-expansions in rare situations leading to '_...	letouzey	2010-09-20
*	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-19
*	Extraction: multiple fixes related with the Not_found encountered by X. Leroy	letouzey	2010-09-17
*	Fix likely semantic typos	glondu	2010-09-15
*	Fix unescaped end-of-lines (OCaml warning 29)	glondu	2010-09-13
*	commit 13400 and 13409.	soubiran	2010-09-13
*	fixed bug #2375 (congruence)	corbinea	2010-09-02
*	Fix [clenv_missing] to compute a better approximation of missing	msozeau	2010-08-02
*	unification des tactiques nsatz pour R Z avec celle des anneaux integres	pottier	2010-07-28
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13338 85f007b7-540e-0...	pottier	2010-07-28
*	nstaz pour les anneaux integres et les setoides, R Z et Q	pottier	2010-07-27
*	Minor fixes:	msozeau	2010-07-27
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	correcting a bug in funind introduced in r 13292	jforest	2010-07-23
*	Extension of the recursive notations mechanism	herbelin	2010-07-22
*	Simplified the way internalization_data (i.e. bindings of bound vars	herbelin	2010-07-22
*	Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).	herbelin	2010-07-22
*	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-18
*	Amelioration dans Function	jforest	2010-07-16
*	fixed bug #2316 (ring_simplify)	barras	2010-07-16
*	Extraction: fix a bit the extraction under modules	letouzey	2010-07-15
*	Fix compilation and test-suite of nsatz	glondu	2010-07-12
*	Extraction: restrict autoinling to csts whose body is globally visible (fix #...	letouzey	2010-07-08
*	Extraction: more factorization of common match branches	letouzey	2010-07-08
*	Extraction: Unset Extraction AutoInline is now the default	letouzey	2010-07-08
*	nsatz in an integral domain with specialization to Z and R	pottier	2010-07-08
*	Extraction Library Foo creates Foo.ml, not foo.ml (correct version)	letouzey	2010-07-07
*	Extraction Library Foo creates Foo.ml, not foo.ml	letouzey	2010-07-07
*	Extraction: get advantage of nicer, algebraic, module types	letouzey	2010-07-07
*	Extraction: some more work on the (re)naming framework	letouzey	2010-07-07
*	Extraction: (yet another) rework of the renaming code	letouzey	2010-07-05
*	Extraction: better support of modules	letouzey	2010-07-02
*	Extraction: no more MPself hence no need for subst during pp	letouzey	2010-07-02
*	Move [delayed] to util and use [force_delayed] everywhere to force	msozeau	2010-06-30
*	Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.	msozeau	2010-06-30