coq - The formal proof system

Age	Commit message (Expand)	Author
2004-01-22	Correction lecture des locations si pas demandees dans l'ordre	herbelin
2004-01-22	Protection table des locations lors de Load (pour coqdoc)	herbelin
2004-01-22	fixes argument lists for tactic definitions, updates inversion tactics	bertot
2004-01-22	adds a clause argument to symmetry	bertot
2004-01-22	corrects the way the structural argument declaration is handled in	bertot
2004-01-22	adds the notations in inductive definitions, improves the consistency between	bertot
2004-01-22	handles explicit function calls, names meta variables in patterns	bertot
2004-01-22	maj	filliatr
2004-01-22	maj	filliatr
2004-01-21	MAJ	herbelin
2004-01-21	Export information des references et location de notations pour coqdoc	herbelin
2004-01-21	Export information des references de notations pour coqdoc	herbelin
2004-01-21	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-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