coq - The formal proof system

Age	Commit message (Expand)	Author
2009-02-06	pushed evar reduction in kernel	barras
2009-02-03	Allow to turn contrib/subtac into a (nat)dynlink'able plugin	letouzey
2009-01-27	Forgot a file in r11859. Sorry...	puech
2009-01-23	Petit nettoyage faisant suite au commit #11847 .	aspiwack
2009-01-22	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-19	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-18	Getting rid of the previous implementation of setoid_rewrite which was	msozeau
2009-01-18	Last changes in type class syntax:	msozeau
2009-01-17	DISCLAIMER	puech
2009-01-14	Fixing #1960 (xml bug with external on goal variable) and #1961	herbelin
2009-01-04	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-01	Switched to "standardized" names for the properties of eq and	herbelin
2008-12-31	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin
2008-12-30	- Fixed bugs and compatibilities issues in	herbelin
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-12-28	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin
2008-12-26	11715 continued	herbelin
2008-12-24	- coq_makefile: target install now respects the original tree structure	herbelin
2008-12-19	Nettoyage des variables Coq et amélioration de coqmktop. Les	notin
2008-12-18	Désactivation de dumpglob lors des appels a functional induction (erreurs pa...	notin
2008-12-17	Avoid printing that extraction has created file Foo when it's not the case	letouzey
2008-12-16	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-14	Generalized binding syntax overhaul: only two new binders: `() and `{},	msozeau
2008-12-10	Bug in 11662 (did not notice that dp_zenon.mll should be modified instead of	herbelin
2008-12-09	About "apply in":	herbelin
2008-12-04	Correct handling of defined methods (let-ins) in instance declarations.	msozeau
2008-11-27	fixed non-exhaustive pattern matching	barras
2008-11-24	amelioration mineur du comportement de Function	jforest
2008-11-23	first attempt to allow Function to deal with dependent pattern matching. This...	jforest
2008-11-22	Fixed bug in VernacExtend printing + missing vernacular printing rules +	herbelin
2008-11-20	correction of bug #2002	jforest
2008-11-09	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-07	Add the ability to give a specific tactic to solve each obligation in	msozeau
2008-11-06	Cosmetic: no more whitespace at end of lines in extraction files	letouzey
2008-11-05	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-10-26	Fixes and refinements regarding occurrence selection:	herbelin
2008-10-26	adding an option Function_raw_tcc to Function	jforest
2008-10-23	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