coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	commande Timeout + compaction des traces de debug_tactic	barras	2009-03-04
*	Les records déclarés avec Record ne peuvent plus être récursifs (le	aspiwack	2009-01-19
*	Backporting from v8.2 to trunk:	herbelin	2009-01-18
*	Getting rid of the previous implementation of setoid_rewrite which was	msozeau	2009-01-18
*	DISCLAIMER	puech	2009-01-17
*	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
*	- coq_makefile: target install now respects the original tree structure	herbelin	2008-12-24
*	Generalized binding syntax overhaul: only two new binders: `() and `{},	msozeau	2008-12-14
*	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
*	More factorization of inductive/record and typeclasses: move class	msozeau	2008-11-09
*	Move Record desugaring to constrintern and add ability to use notations	msozeau	2008-11-05
*	Nouvelle syntaxe pour écrire des records (co)inductifs :	aspiwack	2008-11-05
*	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin	2008-10-11
*	Minor fixes related to coqdoc and --interpolate and the dependent	msozeau	2008-10-03
*	Add user syntax for creating hint databases [Create HintDb foo	msozeau	2008-09-14
*	In manual implicit arguments mode, do not enrich implicits	msozeau	2008-09-14
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Fixes in generalize_eqs/dependent induction to allow the user to specify	msozeau	2008-07-28
*	Suite commit 11236	notin	2008-07-24
*	Correct implementation of discharging of implicit arguments and add new	msozeau	2008-07-22
*	Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...	notin	2008-07-18
*	Affichage intempestif d'information de globalisation + numéro de version dan...	notin	2008-07-18
*	fixed indentation of subgoals for Show Script	barras	2008-07-17
*	Uniformisation du format des messages d'erreur (commencent par une	herbelin	2008-07-17
*	Suite de la révision #11212	notin	2008-07-08
*	Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...	notin	2008-07-07
*	- Improve [Context] vernacular to allow arbitrary binders, not just	msozeau	2008-07-07
*	Lissage de la gestion des chemins de chargement de fichiers :	herbelin	2008-06-29
*	Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...	notin	2008-06-25
*	Enhancements to coqdoc, better globalization of sections and modules.	msozeau	2008-06-06
*	Fix setoid_rewrite documentation examples.	msozeau	2008-06-03
*	Improvements on coqdoc by adding more information into .glob	msozeau	2008-05-30
*	- Nouvelle option "Set Printing Existential Instances" pour forcer	herbelin	2008-05-25
*	Strategy commands are now exported	barras	2008-05-22
*	refined the conversion oracle	barras	2008-05-21
*	- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used to	msozeau	2008-05-12
*	Correction bug #1842 + correction bug initialisation introduit dans	herbelin	2008-05-10
*	Efficacité, bugs, robustesse CoqIDE	herbelin	2008-05-08
*	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin	2008-04-25
*	- Add "Global" modifier for instances inside sections with the usual	msozeau	2008-04-15
*	Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.	msozeau	2008-04-12
*	- Retour en arrière sur la capacité du nouvel apply à utiliser les	herbelin	2008-04-05
*	Add the ability to specify the implicit status of section variables and	msozeau	2008-04-02
*	Fix a bug found by B. Grégoire when declaring morphisms in module	msozeau	2008-03-23
*	Do another pass on the typeclasses code. Correct globalization of class	msozeau	2008-03-19
*	Syntax changes in typeclasses, remove "?" for usual implicit arguments	msozeau	2008-03-06
*	Proper implicit arguments handling for assumptions	msozeau	2008-02-26
*	Merge with lmamane's private branch:	lmamane	2008-02-22