coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Factorisation des produits de même type; parenthèses autour des x:=c et n:=...	herbelin	2003-04-29
*	Factorisation des produits de même type; parenthèses autour des x:=c et n:=...	herbelin	2003-04-29
*	Ajout is_ident_tail	herbelin	2003-04-29
*	Localisation erreurs TacAlias; Globalisation moins tolérante dans les	herbelin	2003-04-28
*	Affichage des Fix contenant des Let dans leur context (ce que la tactique Fix...	herbelin	2003-04-27
*	Reparation affichage LetTac	herbelin	2003-04-27
*	extension des caracteres UTF 8 autorises dans les symboles	filliatr	2003-04-25
*	Ajout "at next level" dans Notation	herbelin	2003-04-17
*	simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...	letouzey	2003-04-16
*	Localisation des appels de tactiques définies sans arguments	herbelin	2003-04-14
*	Correction bug PR#278	coq	2003-04-14
*	Ajout option 'Local' à Infix et Notation	herbelin	2003-04-11