coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	compat ocaml 3.03	filliatr	2001-12-13
*	Retablissement de la commande Existential que j'avais supprime par erreur.	clrenard	2001-11-23
*	Diverses petites simplications de la machine de preuves.	clrenard	2001-11-19
*	Prise en compte qualid dans Hint Unfold	herbelin	2001-09-13
*	ajout Show Intro(s)	letouzey	2001-07-04
*	Fix de quelques bugs syntaxiques de Ltac	delahaye	2001-06-11
*	Uniformisation des 'Save def_tok id'	herbelin	2001-04-09
*	renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...	filliatr	2001-04-04
*	entetes	filliatr	2001-03-15
*	Factorisation du '.' final	herbelin	2001-01-27
*	Prise en compte des noms longs dans les Hints et les Coercions	herbelin	2001-01-24
*	Meta Definition + Tactic Definition	delahaye	2001-01-09
*	Arite cachee de Match Context + Meta Definition	delahaye	2001-01-05
*	Ajout du Let pour le langage de tactiques	delahaye	2000-12-29
*	Nouveau mode de compilation de .ml4	herbelin	2000-11-05
*	Déplacement d'une partie de g_vernac.ml4 dans g_proofs.ml4 car fichier deven...	herbelin	2000-11-05