coq - The formal proof system

Age	Commit message (Expand)	Author
2004-01-20	coqide utf8	marche
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-20	maj	filliatr
2004-01-19	handles projector notations, cases with return types,	bertot
2004-01-19	1.20	bertot
2004-01-19	1.19	bertot
2004-01-19	adds constructs to handle notations in patterns	bertot
2004-01-19	maj	filliatr
2004-01-17	maj	filliatr
2004-01-16	ajoute une option -linkall dans compilation de bin/parser pour assurer que	bertot
2004-01-16	Corrige: Intros [] etait traduit intros (), qui ne reparse pas	barras
2004-01-16	maj	filliatr
2004-01-15	translation to structures now okay for pattern matching constructs	bertot
2004-01-15	Ajout nouvelles options	herbelin
2004-01-15	Ajout load-vernac-source-verbose	herbelin
2004-01-15	maj	filliatr
2004-01-15	maj	filliatr
2004-01-14	compact nested universal quantifications into a single quantification with	bertot
2004-01-14	make sure the parser for FORMULA does not require them to be enclosed in	bertot
2004-01-14	Now, the grammar extension from .v files are concentrated in just a few	bertot
2004-01-14	make libraries, lexing of more utf8 symbols	marche
2004-01-14	maj	filliatr
2004-01-13	MAJ	herbelin
2004-01-13	Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a...	herbelin
2004-01-13	Suppression de Rsyntax en v8	herbelin
2004-01-13	Reference obsolete au niveau 200 de pattern	herbelin
2004-01-13	maj	filliatr
2004-01-12	Set is not always impredicative	barras
2004-01-12	maj	filliatr
2004-01-10	maj	filliatr
2004-01-10	maj	filliatr
2004-01-09	bugs avec Pose et Assert	barras
2004-01-09	Commentaires en v8	herbelin
2004-01-09	Retrait de la notation '^' pour 'power' en V7 car sinon confusion avec la syn...	herbelin
2004-01-09	maj	filliatr
2004-01-08	Finalisation du mecanisme de creation du rpm coqide	herbelin
2004-01-08	Ajout cible install-ide	herbelin
2004-01-08	maj	filliatr
2004-01-07	Vieille syntaxe	herbelin
2004-01-07	Cible redondante qui trouble les make non linux	herbelin
2004-01-07	maj	filliatr
2004-01-06	Version 1 pour coqide	herbelin
2004-01-06	pas ide	herbelin
2004-01-06	MAJ rpm	herbelin
2004-01-06	MAJ	herbelin
2004-01-06	MAJ	herbelin
2004-01-06	maj	filliatr
2004-01-05	Defaut d'information affichage en cas de notation incompatible	herbelin
2004-01-05	certains id n'etaient pas renommes pour eviter les conflits avec les mots-cles	barras