coq - The formal proof system

Age	Commit message (Expand)	Author
2004-02-19	makes sure the following examples are well-treated:	bertot
2004-02-18	- fixed the Assert_failure error in kernel/modops	barras
2004-02-16	accomodate the .. extension	bertot
2004-02-13	adds the possibility to have terms (and not just identifiers) as hints	bertot
2004-02-12	Implicits can have an optional list of argument, which is different	bertot
2004-02-02	adds the possibility to mark function arguments as formulas in Ltac	bertot
2004-01-30	updates the definition of tactics using Ltac and adds the subst tactic	bertot
2004-01-29	updates the tactics contradiction and autorewrite, the commands	bertot
2004-01-28	make sure that 'in' clauses for reduction tactics are translated	bertot
2004-01-26	a try to make intro patterns better	bertot
2004-01-24	streamlines the keywords for definitions, require commandsbinders, notation	bertot
2004-01-22	change add path commands to get the extra argument and the Hint commands	bertot
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