coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Fixed bug in VernacExtend printing + missing vernacular printing rules +	herbelin	2008-11-22
*	correction of bug #2002	jforest	2008-11-20
*	f_equal : solve an inefficiency issue (apply vs. simple apply)	letouzey	2008-11-09
*	better fix for #1931 by using sort_of	letouzey	2008-11-09
*	More factorization of inductive/record and typeclasses: move class	msozeau	2008-11-09
*	Add the ability to give a specific tactic to solve each obligation in	msozeau	2008-11-07
*	Cosmetic: no more whitespace at end of lines in extraction files	letouzey	2008-11-06
*	Move Record desugaring to constrintern and add ability to use notations	msozeau	2008-11-05
*	Suite commit 11539 sur notation Record dans (Co)Inductive (MAJ	herbelin	2008-11-05
*	Nouvelle syntaxe pour écrire des records (co)inductifs :	aspiwack	2008-11-05
*	Better extraction renaming phase (fix #1914 plus other non-reported bugs)	letouzey	2008-11-05
*	Fixes and refinements regarding occurrence selection:	herbelin	2008-10-26
*	adding an option Function_raw_tcc to Function	jforest	2008-10-26
*	Fix bug #1977 by allowing the [apply] variants to take an [open_constr]	msozeau	2008-10-23
*	Open notation for declaring record instances.	msozeau	2008-10-23
*	Generalized implementation of generalization.	msozeau	2008-10-23