coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...	filliatr	2001-04-04
*	entetes	filliatr	2001-03-15
*	Prise en compte noms longs dans Implicits	herbelin	2001-02-16
*	Bug point final dans la syntaxe theorem_body	herbelin	2001-02-09
*	Correction pour Time pour ne pas etre oblige de mettre deux points	delahaye	2001-02-05
*	Factorisation du '.' final	herbelin	2001-01-27
*	Prise en compte des noms longs dans les Hints et les Coercions	herbelin	2001-01-24
*	Ajout de constantes locales dans les Records	herbelin	2001-01-24
*	Ajout du Let pour le langage de tactiques	delahaye	2000-12-29
*	ajout ident_or_constrarg pour NewInduction	herbelin	2000-12-20
*	Begin-End Silent deviennent Set?Unset Silent	mohring	2000-11-21
*	Prise en compte des noms qualifiés dans certaines commandes	herbelin	2000-11-20
*	Déplacement d'une partie de g_vernac.ml4 dans g_proofs.ml4 car fichier deven...	herbelin	2000-11-05
*	compilation des fichiers ml4 sans GNUseries	filliatr	2000-11-03
*	Priorite du Try/Orelse + Debug switch + correction bug dans Pattern	delahaye	2000-10-30
*	Pattern matching de sous-termes + exceptions dans le lexer	delahaye	2000-08-17
*	Ajout syntaxe [ phr1 ... phrn ]. pour grouper des commandes (pour Time ou Gra...	herbelin	2000-07-26
*	':>' est devenu un seul token	herbelin	2000-06-02
*	Ajout du langage de tactiques	delahaye	2000-05-03
*	Bête renommage	herbelin	2000-01-20
*	Nettoyage des fichiers de parsing	herbelin	2000-01-13
*	Renommage command en constr	herbelin	2000-01-07
*	Les inductifs dans Scheme doivent être des ident d'inductifs	herbelin	1999-12-15
*	modules et coqc	filliatr	1999-12-12
*	- erreurs Pretype	filliatr	1999-12-10
*	debug discharge et inductifs	filliatr	1999-12-10
*	Intégration du Termast et du Retyping de HH, et modifications connexes	herbelin	1999-12-01
*	compilation des grammaires (ouf)	filliatr	1999-09-08
*	modules grammaire Coq	filliatr	1999-09-08