coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Nettoyage et documentation de Library	herbelin	2005-02-06
*	pb install de pcoq	barras	2004-04-21
*	adds a new command add_rec_path for the parser program and changes add_path	bertot	2004-02-13
*	make sure the parser for FORMULA does not require them to be enclosed in	bertot	2004-01-14
*	Correction du bug 335 et Export/Require Export dans un module	coq	2003-10-07
*	Ajout 'Close Scope', mise en place de la structure pour un modificateur 'format'	herbelin	2003-09-30
*	Make sure that identifiers are parsed as qualified identifier and that	bertot	2003-03-06
*	The data constructed when detecting an error in a list of commands must	bertot	2003-01-24
*	Take notations into account: numbers and the CNotation operator.	bertot	2002-12-09
*	Modification Require From	mohring	2002-12-04
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Changé le nom du module Errors (errors.mli, errors.ml) en Cerrors parce	ddr	2002-02-20
*	Plusieurs arguments autorisés pour Require et Read Module	herbelin	2002-01-18
*	Integrating the Ltac language and the Blast tool into the interface	bertot	2001-12-18
*	compat ocaml 3.03	filliatr	2001-12-13
*	GROS COMMIT:	barras	2001-11-05
*	Abstraction de l'immplementation de dirpath et implementation dans l'autre se...	herbelin	2001-10-17
*	Prsing	herbelin	2001-08-10
*	Adding files for the production of textual explanations as used in pcoq.	bertot	2001-04-18
*	renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...	filliatr	2001-04-04
*	These files are used to construct an independent parser, that is a small	bertot	2001-04-04