coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	fixed ring/field warning about hyp cleaning up	barras	2009-03-18
*	Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)	herbelin	2009-03-17
*	- gros commit sur ring et field: passage des arguments simplifie	barras	2009-03-17
*	Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"	herbelin	2009-03-16
*	Cleaning/uniformizing the interface of tacticals.mli	herbelin	2009-03-14
*	Makefile: ml dependencies of contribs are moved to .mllib files	letouzey	2009-03-14
*	Cleanup: remove old correctness files, unused for a long time	letouzey	2009-03-11
*	fixed groebner as a plugin + pattern matching Timeout	barras	2009-03-06
*	missing Require	barras	2009-03-06
*	oups (module Entiers remplace par Big_int)	barras	2009-03-06
*	ajout de la tactique groebner de Loic Pottier	barras	2009-03-05
*	Backtrack sur la mémoïsation de nf_evar.	aspiwack	2009-03-04
*	=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...	aspiwack	2009-02-27
*	extraction: update of README+CHANGES, rm of BUGS+TODO	letouzey	2009-02-27
*	coq-interface and coq-parser can be calls to coqtop with adequate code dynlink	letouzey	2009-02-20
*	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack	2009-02-19
*	pushed evar reduction in kernel	barras	2009-02-06
*	Allow to turn contrib/subtac into a (nat)dynlink'able plugin	letouzey	2009-02-03
*	Forgot a file in r11859. Sorry...	puech	2009-01-27
*	Petit nettoyage faisant suite au commit #11847 .	aspiwack	2009-01-23
*	Fix #2011 : an incorrect environment when extracting Module ... with ...	letouzey	2009-01-22
*	Extraction Library works now when some files share the same short name (fix #...	letouzey	2009-01-22
*	Les records déclarés avec Record ne peuvent plus être récursifs (le	aspiwack	2009-01-19
*	- Structuring Numbers and fixing Setoid in stdlib's doc.	herbelin	2009-01-19
*	Getting rid of the previous implementation of setoid_rewrite which was	msozeau	2009-01-18
*	Last changes in type class syntax:	msozeau	2009-01-18
*	DISCLAIMER	puech	2009-01-17
*	Fixing #1960 (xml bug with external on goal variable) and #1961	herbelin	2009-01-14
*	Moved JProver to a user contribution (as was decided a long time ago)	herbelin	2009-01-04
*	Fixed bugs #2001 (search_guard was overwriting the guard index given	herbelin	2009-01-04
*	Switched to "standardized" names for the properties of eq and	herbelin	2009-01-01
*	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin	2008-12-31
*	- Fixed bugs and compatibilities issues in	herbelin	2008-12-30
*	- Added support for subterm matching in SearchAbout.	herbelin	2008-12-29
*	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin	2008-12-28
*	11715 continued	herbelin	2008-12-26
*	- coq_makefile: target install now respects the original tree structure	herbelin	2008-12-24
*	Nettoyage des variables Coq et amélioration de coqmktop. Les	notin	2008-12-19
*	Désactivation de dumpglob lors des appels a functional induction (erreurs pa...	notin	2008-12-18
*	Avoid printing that extraction has created file Foo when it's not the case	letouzey	2008-12-17
*	Extraction Blacklist : a new command for avoiding conflicts with existing files	letouzey	2008-12-16
*	Extraction: also comply to Set Printing Width when producing external files	letouzey	2008-12-16
*	Take advantage of natdynlink when available: almost all contribs become loada...	letouzey	2008-12-16
*	Generalized binding syntax overhaul: only two new binders: `() and `{},	msozeau	2008-12-14
*	Bug in 11662 (did not notice that dp_zenon.mll should be modified instead of	herbelin	2008-12-10
*	About "apply in":	herbelin	2008-12-09
*	Correct handling of defined methods (let-ins) in instance declarations.	msozeau	2008-12-04
*	fixed non-exhaustive pattern matching	barras	2008-11-27
*	amelioration mineur du comportement de Function	jforest	2008-11-24
*	first attempt to allow Function to deal with dependent pattern matching. This...	jforest	2008-11-23