coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	Fixing/improving management of uniform prefix Local and Global	herbelin	2009-01-14
*	- Standardized prefix use of "Local"/"Global" modifiers as decided in	herbelin	2009-01-13
*	- Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).	herbelin	2009-01-11
*	Conversion du fichier 'revision' en un fichier .ml + correction d'un bug dans...	notin	2009-01-06
*	Completed 11745 (move of jprover to user contribs) and cleaned 11743	herbelin	2009-01-05
*	Bug dans commit 11743	herbelin	2009-01-04
*	Fixed bugs #2001 (search_guard was overwriting the guard index given	herbelin	2009-01-04
*	Made the debugger work again:	herbelin	2009-01-02
*	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin	2008-12-31
*	- Added support for subterm matching in SearchAbout.	herbelin	2008-12-29
*	- Suppression date dans configure du trunk	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
*	Sequel of 11697: repair coqtop.byte when contribs are statically linked (+min...	letouzey	2008-12-17
*	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
*	About "apply in":	herbelin	2008-12-09
*	Correct handling of defined methods (let-ins) in instance declarations.	msozeau	2008-12-04
*	Inductive parameters: nicer doc examples and error message	letouzey	2008-11-28
*	- Synchronized subst_object with load_object (load_and_subst_objects)	herbelin	2008-11-23
*	Minor improvement to commit 11619	herbelin	2008-11-23
*	Fixed bug #2006 (type constraint on Record was not taken into account) +	herbelin	2008-11-23
*	Fixed bug in VernacExtend printing + missing vernacular printing rules +	herbelin	2008-11-22
*	- Fixed minor bug #1994 in the tactic chapter of the manual [doc]	herbelin	2008-11-22
*	Tentative d'amélioration de la robustesse des Makefile générés par	notin	2008-11-13
*	Fix mixup between Record, Structure and Class by adding a new variant for	msozeau	2008-11-10
*	More factorization of inductive/record and typeclasses: move class	msozeau	2008-11-09
*	- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in	herbelin	2008-11-09
*	Slight change of the semantics of user-given casts: they don't really	msozeau	2008-11-07
*	Fix in the unification algorithm using evars: unify types of evar	msozeau	2008-11-05
*	Move Record desugaring to constrintern and add ability to use notations	msozeau	2008-11-05
*	Petit bug dans le commit précédent.	aspiwack	2008-11-05
*	Nouvelle syntaxe pour écrire des records (co)inductifs :	aspiwack	2008-11-05
*	Remove calls to Dynlink.add_{interfaces,available_units} altogether	glondu	2008-10-29
*	Native "Declare ML Module" when possible	glondu	2008-10-28
*	11511 continued (bug in set.out + incohérence dans "Theorem with"	herbelin	2008-10-28
*	- Fixed many "Theorem with" bugs.	herbelin	2008-10-27
*	Fixes and refinements regarding occurrence selection:	herbelin	2008-10-26
*	- MAJ svn:ignore pour bin/coq-parser (anciennement bin/parser)	herbelin	2008-10-26
*	Raise informative errors instead of Failures or anomalies in case a meta	msozeau	2008-10-24
*	Open notation for declaring record instances.	msozeau	2008-10-23
*	Generalized implementation of generalization.	msozeau	2008-10-23
*	Fix bugs #1975 and #1976.	msozeau	2008-10-22
*	Affichage des notations récursives:	herbelin	2008-10-22
*	- Export de pattern_ident vers les ARGUMENT EXTEND and co.	herbelin	2008-10-19
*	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin	2008-10-11