coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ajout 'Print Scopes' et 'Bind Scope with classes'	herbelin	2003-09-12
*	MAJ module requis pour le parsing des numéraux	herbelin	2003-09-12
*	Affichage des scopes d'arguments	herbelin	2003-09-12
*	Ajout 'Print Scopes' et 'Bind Scope with classes'; 'Delimits' -> 'Delimit'	herbelin	2003-09-12
*	Passage des projections au niveau 1	herbelin	2003-09-10
*	9 est associatif a gauche	herbelin	2003-09-10
*	Traduction de Distfix	herbelin	2003-09-10
*	Ajout construction If primitive dans constr_expr et rawconstr	herbelin	2003-09-09
*	'Grammar tactic' devient 'Tactic Notation'	herbelin	2003-09-09
*	Traduction des réferences arguments de commandes non primitives	herbelin	2003-09-09
*	Code mort	herbelin	2003-09-09
*	Mise en place possibilité de définitions locales dans les paramètres des r...	herbelin	2003-09-06
*	Mise en place possibilité de définitions locales dans les paramètres des r...	herbelin	2003-09-06
*	Paramétrisation vis à vis de existential_key	herbelin	2003-09-06
*	'Implicits qid' -> 'Implicit Arguments qid'	herbelin	2003-09-06
*	Adapter l'entree de grammaire a la version 7 ou 8	herbelin	2003-09-06
*	Mise en place possibilité de définitions locales dans les paramètres des i...	herbelin	2003-09-06
*	Passage de lconstr à constr pour les arguments immédiat de commandes	herbelin	2003-09-06
*	Passage de lconstr à constr pour les arguments immédiat de commandes	herbelin	2003-09-06
*	Bug affichage tactiques supplementaires en v8 (suite)	herbelin	2003-09-06
*	Bug affichage tactiques supplementaires en v8	herbelin	2003-09-05
*	Impression sans ',' des constructeurs de meme type, pour v8	herbelin	2003-09-05
*	Relachement conflit 'with' dans le cas des Module with Definition	herbelin	2003-09-02
*	'Assumptions' sur le modèle général des lieurs	herbelin	2003-08-31
*	Affichage des inductifs en v8	herbelin	2003-08-31
*	Pb de mot-cle	herbelin	2003-08-14
*	Ajout token '!' pour correctness	herbelin	2003-08-14
*	Enregistrement tuple_constr	herbelin	2003-08-14
*	Nouvelle mouture du traducteur v7->v8	herbelin	2003-08-11
*	Bug compilation	herbelin	2003-06-20
*	Ajout 'Symmetry in Hyp'	herbelin	2003-06-19
*	Ajout 'Symmetry in Hyp'; chgt syntaxe 'change ... with ...'	herbelin	2003-06-19
*	Ajout option Local aux Hint	herbelin	2003-06-17
*	Ajout option Local à Hint, Hints et HintDestruct	herbelin	2003-06-14
*	Utilisation de intro_pattern dans NewDestruct/NewInduction	herbelin	2003-06-13
*	Token '.(' seulement pour v8, sinon conflit avec '.(*'	herbelin	2003-06-11
*	Ajout notation c.(f) en v8 pour les projections de Record	herbelin	2003-06-10
*	freshid -> fresh	herbelin	2003-06-10
*	Tables logarithmiques pour les coercions + nettoyage	herbelin	2003-06-08
*	Bug	herbelin	2003-05-26
*	Ajout FreshId	herbelin	2003-05-24
*	Ajout V8Notation	herbelin	2003-05-22
*	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin	2003-05-21
*	Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...	herbelin	2003-05-21
*	Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...	herbelin	2003-05-21
*	Possibilité de syntaxe conjointement à la définition des inductifs et des ...	herbelin	2003-05-21
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Petite correction d'affichage de modules	coq	2003-05-08
*	Prise en compte des syntaxes v8 dans Uninterpreted Notation	herbelin	2003-04-29
*	Prise en compte des syntaxes v8 dans Uninterpreted Notation	herbelin	2003-04-29