coq - The formal proof system

Age	Commit message (Expand)	Author
2010-08-02	Fix [clenv_missing] to compute a better approximation of missing	msozeau
2010-07-28	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-27	nstaz pour les anneaux integres et les setoides, R Z et Q	pottier
2010-07-27	Minor fixes:	msozeau
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-07-23	correcting a bug in funind introduced in r 13292	jforest
2010-07-22	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-18	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-16	Amelioration dans Function	jforest
2010-07-16	fixed bug #2316 (ring_simplify)	barras
2010-07-15	Extraction: fix a bit the extraction under modules	letouzey
2010-07-12	Fix compilation and test-suite of nsatz	glondu
2010-07-08	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-07	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-05	Extraction: (yet another) rework of the renaming code	letouzey
2010-07-02	Extraction: better support of modules	letouzey
2010-07-02	Extraction: no more MPself hence no need for subst during pp	letouzey
2010-06-30	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-29	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-28	Extraction: handling modules (not functors) in Haskell by name mangling	letouzey
2010-06-28	Extraction: remove a useless match	letouzey
2010-06-25	bug 2328 fixed: failure when polynomial not i ideal	pottier
2010-06-23	Extraction: nicer simple extraction of custom defs (fix #2204)	letouzey
2010-06-23	Names: remove obsolete mod_self_id	letouzey
2010-06-21	Extraction: replace unicode characters in ident by ascii encodings (fix #2158...	letouzey
2010-06-16	Extraction: fix the eta reduction function used in code optimisations	letouzey
2010-06-15	Extraction: in support library, more and nicer big_int	letouzey
2010-06-14	Fixed commit 13125 (stricter check of induction args): an interpretation	herbelin
2010-06-12	Fixing spelling: pr_coma -> pr_comma	herbelin
2010-06-10	Extraction Implicits: can accept argument names instead of just positions	letouzey
2010-06-09	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-08	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