coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Deplacement lexer pour dependance dans constrintern	herbelin	2004-01-21
*	updates the structure of fix (struct argument added) and if	bertot	2004-01-21
*	MAJ	herbelin	2004-01-21
*	maj	filliatr	2004-01-21
*	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-20
*	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-19
*	maj	filliatr	2004-01-17
*	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-16
*	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-15
*	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-14
*	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-13
*	Set is not always impredicative	barras	2004-01-12
*	maj	filliatr	2004-01-12
*	maj	filliatr	2004-01-10
*	maj	filliatr	2004-01-10
*	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-09
*	Finalisation du mecanisme de creation du rpm coqide	herbelin	2004-01-08
*	Ajout cible install-ide	herbelin	2004-01-08
*	maj	filliatr	2004-01-08
*	Vieille syntaxe	herbelin	2004-01-07
*	Cible redondante qui trouble les make non linux	herbelin	2004-01-07
*	maj	filliatr	2004-01-07
*	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