coq - The formal proof system

Age	Commit message (Expand)	Author
2004-01-26	reparation de qqs bugs du traducteur	barras
2004-01-22	Protection table des locations lors de Load (pour coqdoc)	herbelin
2004-01-21	Export information des references et location de notations pour coqdoc	herbelin
2004-01-20	Le traducteur utilisait un afficheur des reels obsolete et bugge	herbelin
2004-01-20	Suppression 'Implicit Arguments On/Off' qui n'a plus lieu d'etre en v8	herbelin
2004-01-14	make libraries, lexing of more utf8 symbols	marche
2004-01-13	Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a...	herbelin
2004-01-13	Reference obsolete au niveau 200 de pattern	herbelin
2004-01-09	bugs avec Pose et Assert	barras
2004-01-02	meilleure presentation des commentaires du traducteur	barras
2003-12-24	Bug affichage Decompose	herbelin
2003-12-23	* empty log message *	barras
2003-12-22	Mise en valeur intropattern de paires et acceptation dans le 'as' de inductio...	herbelin
2003-12-19	Substitution dans REvar et PEvar plutot que encodage via noeud application po...	herbelin
2003-12-19	name_app accessible a tous dans Nameops	herbelin
2003-12-17	ajout test de non-regression Clear d'une def locale	barras
2003-12-16	MAJ suppression 250	herbelin
2003-12-15	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras
2003-12-08	correction bug: parentheses ne cassent plus les implicites	barras
2003-12-04	Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace p...	herbelin
2003-12-04	Symetrisation parsing/printing 'abstract'	herbelin
2003-12-01	Nouvelle tactique EExists	clrenard
2003-11-27	Ajout ne_string	herbelin
2003-11-26	Protection contre les notations vides	herbelin
2003-11-26	Traduction de tactic:constrarg en constr:constr pour les arguments de Tactic ...	herbelin
2003-11-25	modif lexer: ident peut commencer par _	barras
2003-11-25	Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...	herbelin
2003-11-23	Prise en compte des definitions locales dans les (co-)points-fixes	herbelin
2003-11-21	Suppression des niveaux vides	herbelin
2003-11-21	Ajout Print Implicit	herbelin
2003-11-21	Pas d'entrees autres que les predefinies en v8	herbelin
2003-11-20	Nouvelle solution pour le probleme d'effacement des niveaux vides de opercons...	herbelin
2003-11-19	Distinction entre 'as _' qui cache le terme filtre (si variable) et rien dans...	herbelin
2003-11-19	Protection contre l'effacement des niveaux vides de operconstr et pattern par...	herbelin
2003-11-18	reparation bug moins unaire (erreur de PP)	barras
2003-11-18	Code mort	herbelin
2003-11-17	New tactics : econstructor, eleft, eright, esplit	clrenard
2003-11-17	Inteprétation des idents filtrés liants dans constrintern.ml (plus robuste)	herbelin
2003-11-15	Bug v8 (regles connues etaient re-enregistrees) + tables dans egrammar	herbelin
2003-11-15	Ajout Print Implicit avec depliage du type	herbelin
2003-11-14	Compatibilite %T	herbelin
2003-11-14	Bug parsing cast	herbelin
2003-11-13	moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...	barras
2003-11-13	factorisation et generalisation des clauses	barras
2003-11-12	Suppression du "..." final !	herbelin
2003-11-12	Mise en place systeme de renommage des noms de variables liees dans la biblio...	herbelin
2003-11-12	MAJ ZArith; contraintes plus faibles pour decider la capacite a interpreter l...	herbelin
2003-11-12	Idtac peut prendre un argument à afficher	narboux
2003-11-12	petits changements de syntaxe	barras
2003-11-10	Suppression SearchNamed finalement redondant avec SearchAbout	herbelin