coq - The formal proof system

Age	Commit message (Expand)	Author
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-21	updates the structure of fix (struct argument added) and if	bertot
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-15	translation to structures now okay for pattern matching constructs	bertot
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-13	Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a...	herbelin
2004-01-09	bugs avec Pose et Assert	barras
2004-01-02	meilleure presentation des commentaires du traducteur	barras
2003-12-01	Nouvelle tactique EExists	clrenard
2003-11-29	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin
2003-11-25	Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...	herbelin
2003-11-18	correction suite ajout nouvelles tactiques	clrenard
2003-11-15	Ajout Print Implicit avec depliage du type	herbelin
2003-11-13	factorisation et generalisation des clauses	barras
2003-11-12	Bug TacId	herbelin
2003-11-10	Suppression SearchNamed finalement redondant avec SearchAbout	herbelin
2003-11-09	Traduction semantique des InHyp de clause en InHypValue si local def	herbelin
2003-11-06	Added Instantiate ... in	corbinea
2003-11-01	Ajout CPatNotation, PrintVisibility	herbelin
2003-10-23	Conjecture declare maintenant un axiome; reorganisation VernacDefinition	herbelin
2003-10-22	Integration de SearchNamed dans SearchAbout	herbelin
2003-10-22	reorganisation des niveaux (ex: = est a 70)	barras
2003-10-16	nouvelle syntaxe de ltac	barras
2003-10-13	Ajout d'une fonction de recherche sur les composantes du nom des objets	herbelin
2003-10-13	Deplacement next_global_ident_away dans Termops	herbelin
2003-10-13	Ajout d'une fonction de recherche sur les composantes du nom des objets	herbelin
2003-10-10	Cablage en dur de inversion	herbelin
2003-10-10	show_subgoals dans Pfedit	herbelin
2003-10-10	changement nouvelle syntaxe (pt fixes)	barras
2003-10-08	Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...	herbelin
2003-10-07	Correction du bug 335 et Export/Require Export dans un module	coq
2003-09-30	Ajout 'Close Scope', mise en place de la structure pour un modificateur 'format'	herbelin
2003-09-23	Utilisation de noms dans 'Implicit Arguments [...]'	herbelin
2003-09-21	Mise en place d'implicites par noms en v8	herbelin
2003-09-19	parsing	herbelin
2003-09-12	Ajout 'Print Scopes' et 'Bind Scope with classes'	herbelin
2003-09-09	Ajout construction If primitive dans constr_expr et rawconstr	herbelin
2003-09-06	Mise en place possibilité de définitions locales dans les paramètres des r...	herbelin
2003-09-06	Mise en place possibilité de définitions locales dans les paramètres des i...	herbelin
2003-08-11	Nouvelle mouture du traducteur v7->v8	herbelin
2003-06-19	Ajout 'Symmetry in Hyp'	herbelin