coq - The formal proof system

Age	Commit message (Expand)	Author
2004-03-26	Ajout entree pour exporter les commentaires en mode -xml	herbelin
2004-03-25	Code mort	herbelin
2004-03-17	Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...	herbelin
2004-03-17	Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...	herbelin
2004-03-17	Parsing des V8Notation avec motif recursif en v7	herbelin
2004-03-17	Utilisation de '..' pour la notation concrete des motifs recursifs de filtrage	herbelin
2004-03-17	Mise en place de motifs récursifs dans Notation; quelques simplifications au...	herbelin
2004-03-05	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras
2004-03-03	Plus de noms d'entrees de grammaires qualifies dans 'Tactic Notation'	herbelin
2004-03-02	Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...	herbelin
2004-03-02	Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation...	herbelin
2004-03-02	Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...	herbelin
2004-03-02	Correction oubli du cas pas d'arguments implicites du tout	herbelin
2004-03-01	Généralisation du type ltac Identifier en IntroPattern; prise en compte des...	herbelin
2004-02-28	Expansion du type par nécessité dans le cas d'affichage d'implicites	herbelin
2004-02-26	Keep structure information for Fixpoint declaration and Fix terms	bertot
2004-02-21	Correction oubli de report d'une modification de g_vernac (1.69) vers g_verna...	herbelin
2004-02-18	- fixed the Assert_failure error in kernel/modops	barras
2004-02-17	Ajout de lconstr, constr et binder_constr dans Print Grammar constr	herbelin
2004-02-16	export the general function for getting information from the environment	bertot
2004-02-13	Uniformisation du comportement de Notation et Reserved Notation	herbelin
2004-02-12	Localisation des erreurs d'internalisation des notations de tactiques	herbelin
2004-01-29	Suppression de 'Print.' en v8	herbelin
2004-01-29	Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...	herbelin
2004-01-27	Ajout 'as (x,...,y)' dans NewDestruct et NewInd, NewInduction, ...	herbelin
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