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	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	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-09	bugs avec Pose et Assert	barras
2003-11-13	factorisation et generalisation des clauses	barras
2003-10-22	reorganisation des niveaux (ex: = est a 70)	barras
2003-10-16	nouvelle syntaxe de ltac	barras
2003-01-26	all tactics should be covered now: remains	bertot
2003-01-25	Add translations for many tactics but a dozen are still remaining	bertot
2003-01-22	removes all references to ctast.ml the Makefile has been updated accordingly.	bertot
2003-01-21	Add a few operators in the new version of xlate.ml and make sure	bertot
2002-12-09	Ajoute le bon traitement pour Ring, Locate, Comments	bertot
2002-12-09	Take notations into account: numbers and the CNotation operator.	bertot
2002-12-03	Etape intermédiaire d'adaptation de la connexion à pcoq aux nouvelles	bertot
2002-10-06	correcting the treatment of many tactics that use quant_hyp in file xlate.ml	bertot
2002-10-03	Previous version did compile but did not make it possible to actually run	bertot
2001-12-18	Integrating the Ltac language and the Blast tool into the interface	bertot
2001-11-05	GROS COMMIT:	barras
2001-04-18	Adding files for the production of textual explanations as used in pcoq.	bertot
2001-04-04	Files that handle the dialogue with the graphical user-interface pcoq.	bertot