coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Add user syntax for creating hint databases [Create HintDb foo	msozeau	2008-09-14
*	Add the ability to declare [Hint Extern]'s with no pattern.	msozeau	2008-09-07
*	Fixes in typeclasses resolution. Avoid reducing instances types before	msozeau	2008-09-07
*	Syntax changes in typeclasses, remove "?" for usual implicit arguments	msozeau	2008-03-06
*	Merge with lmamane's private branch:	lmamane	2008-02-22
*	Generalized CAMLP4USE for pp dependencies	corbinea	2007-07-16
*	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau	2007-03-19
*	Declarative Proof Language: main commit	corbinea	2006-09-20
*	The "clean integration of subtac" patch.	msozeau	2006-05-29
*	Suppression code pour hints nommés à la V7 (voire à la V6...)	herbelin	2006-01-28
*	Messages de idtac et fail peuvent maintenant être des listes de string, int ...	herbelin	2006-01-21
*	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin	2005-12-26
*	Nouvelle en-tête	herbelin	2004-07-16
*	meilleure presentation des commentaires du traducteur	barras	2004-01-02
*	Idtac peut prendre un argument à afficher	narboux	2003-11-12
*	reorganisation des niveaux (ex: = est a 70)	barras	2003-10-22
*	Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...	herbelin	2003-10-08
*	Debranchement de l'affichage automatique de Proof par le traducteur (trop com...	herbelin	2003-10-07
*	Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...	herbelin	2003-09-12
*	Nouvelle mouture du traducteur v7->v8	herbelin	2003-08-11
*	Ajout option Local à Hint, Hints et HintDestruct	herbelin	2003-06-14
*	Ajout notation c.(f) en v8 pour les projections de Record	herbelin	2003-06-10
*	Utilisation de CAppExpl au lieu de CRef pour les hints pour qu'aucun implicite	herbelin	2003-04-07
*	* empty log message *	barras	2003-03-12
*	Ajout du vernac Proof with	gregoire	2002-12-12
*	Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...	herbelin	2002-11-24
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour	herbelin	2002-07-11
*	Fusion entre la nouvelle et l'ancienne syntaxe de HintDestruct	herbelin	2002-06-05
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	compat ocaml 3.03	filliatr	2001-12-13
*	Retablissement de la commande Existential que j'avais supprime par erreur.	clrenard	2001-11-23
*	Diverses petites simplications de la machine de preuves.	clrenard	2001-11-19
*	Prise en compte qualid dans Hint Unfold	herbelin	2001-09-13
*	ajout Show Intro(s)	letouzey	2001-07-04
*	Fix de quelques bugs syntaxiques de Ltac	delahaye	2001-06-11
*	Uniformisation des 'Save def_tok id'	herbelin	2001-04-09
*	renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...	filliatr	2001-04-04
*	entetes	filliatr	2001-03-15
*	Factorisation du '.' final	herbelin	2001-01-27
*	Prise en compte des noms longs dans les Hints et les Coercions	herbelin	2001-01-24
*	Meta Definition + Tactic Definition	delahaye	2001-01-09
*	Arite cachee de Match Context + Meta Definition	delahaye	2001-01-05
*	Ajout du Let pour le langage de tactiques	delahaye	2000-12-29
*	Nouveau mode de compilation de .ml4	herbelin	2000-11-05
*	Déplacement d'une partie de g_vernac.ml4 dans g_proofs.ml4 car fichier deven...	herbelin	2000-11-05