coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	QArith: typo in name of hint db (fix #2346)	letouzey	2010-06-29
*	change the flag "internal" in declare/ind_tables from bool to	vsiles	2010-06-29
*	Made tclABSTRACT normalize evars before saying it does not support	herbelin	2010-06-29
*	Extraction: handling modules (not functors) in Haskell by name mangling	letouzey	2010-06-28
*	Extraction: remove a useless match	letouzey	2010-06-28
*	bug 2328 fixed: failure when polynomial not i ideal	pottier	2010-06-25
*	Extraction: nicer simple extraction of custom defs (fix #2204)	letouzey	2010-06-23
*	Names: remove obsolete mod_self_id	letouzey	2010-06-23
*	Extraction: replace unicode characters in ident by ascii encodings (fix #2158...	letouzey	2010-06-21
*	Extraction: fix the eta reduction function used in code optimisations	letouzey	2010-06-16
*	Extraction: in support library, more and nicer big_int	letouzey	2010-06-15
*	Fixed commit 13125 (stricter check of induction args): an interpretation	herbelin	2010-06-14
*	Fixing spelling: pr_coma -> pr_comma	herbelin	2010-06-12
*	Extraction Implicits: can accept argument names instead of just positions	letouzey	2010-06-10
*	Fix bug #2262: bad implicit argument number by avoiding counting	msozeau	2010-06-09
*	Allowing to use an ordering different than Lt with measure	jforest	2010-06-09
*	Using vernac parsing for Function	jforest	2010-06-08
*	Extraction with implicits: perform the occur-check after optimisations	letouzey	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 treatment of {struct x} annotations in presence of generalized	msozeau	2010-06-08
*	Added support for Ltac-matching terms with variables bound in the pattern	herbelin	2010-06-06
*	Extraction: attempt to provide nice extraction of chars and strings for Ocaml	letouzey	2010-06-04
*	Extraction: finish ExtrOcamlNatInt, add similar translation nat==>big_int	letouzey	2010-06-04