coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Documentation de "Set Printing Universes", "Print Universes" (anciennement	herbelin	2006-10-28
*	improve the amount of information given by the Ltac tactic debugger	bertot	2006-08-28
*	Amélioration des messages d'erreurs de tacred; unfold considère maintenant le	herbelin	2006-02-07
*	Messages de idtac et fail peuvent maintenant être des listes de string, int ...	herbelin	2006-01-21
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...	herbelin	2005-12-17
*	Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...	herbelin	2005-12-17
*	Abstraction vis à vis du type loc pour compatibilité ocaml 3.08	herbelin	2004-07-16
*	Nouvelle en-tête	herbelin	2004-07-16
*	Adaptation a la v7 du message d'erreur Match_failure	herbelin	2004-03-16
*	search window	coq	2004-02-04
*	Affichage Assert_failure en ocaml 3.07	herbelin	2003-10-28
*	Ajout d'un message à FailTac	herbelin	2003-03-31
*	Debugger plus informatif	delahaye	2003-02-13
*	msg Failtac; echec -batch s'il reste des preuves	filliatr	2003-01-17
*	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
*	resolution du pb d'efficacite du a Sign.add_named_decl	barras	2002-04-04
*	Bug d'affichage des erreurs localisées dans un fichier suite à	herbelin	2002-03-27
*	Changé le nom du module Errors (errors.mli, errors.ml) en Cerrors parce	ddr	2002-02-20