coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Correction du bug 335 et Export/Require Export dans un module	coq	2003-10-07
*	Cacher les .v8	herbelin	2003-10-03
*	Changement de l'afficheur pour que les variables liées aient un nom indépen...	herbelin	2003-09-23
*	Indépendance vis à vis de Declare	herbelin	2003-09-12
*	Mise en place possibilité de définitions locales dans les paramètres des r...	herbelin	2003-09-06
*	Traducteur de correctness	herbelin	2003-08-14
*	code mort	herbelin	2003-08-14
*	Notation access au dessous du niveau applicatif (2eme)	herbelin	2003-08-14
*	Notation access au dessous du niveau applicatif	herbelin	2003-08-13
*	Nouvelle mouture du traducteur v7->v8	herbelin	2003-08-11
*	Ajout notation c.(f) en v8 pour les projections de Record	herbelin	2003-06-10
*	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin	2003-05-21
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Divers	herbelin	2003-04-17
*	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"	herbelin	2003-04-09
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)	herbelin	2003-03-29
*	* Ajout du traducteur nouvelle syntaxe *	barras	2003-03-12
*	Evaluation paresseuse de l'affichage du debug	herbelin	2002-12-15
*	Compensation de suppression betaiota de type_of	herbelin	2002-12-11
*	Normalisation des types (fait avant dans Typing)	herbelin	2002-12-10
*	Court-circuit de g_zsyntax	herbelin	2002-11-28
*	Remplacement Grammar/Syntax par Notation	herbelin	2002-11-26
*	typo	herbelin	2002-11-18
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Intégration des modifs de la branche mowgli :	herbelin	2002-11-05
*	portage Correctness (substitutivité pour les modules)	filliatr	2002-09-19
*	retablissement de Correctness (pas encore teste' cependant)	filliatr	2002-09-18
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulement	filliatr	2002-06-21
*	ZArith_base, Zbool, Bool_nat	filliatr	2002-06-20
*	ProgWf -> Zwf	filliatr	2002-06-19
*	deplacement contrib/correctness/ProgWf -> theories/ZArith/Zwf	filliatr	2002-06-19
*	Protection des tactiques contre l'utilisation sans le bon contexte de thories	herbelin	2002-06-03
*	Factorisation de 'Show Programs' au premier niveau de Vernac_.command	herbelin	2002-06-03
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Fichiers contrib//.ml4 remplacent les contrib//.v	herbelin	2002-05-29
*	Uniformisation (Qed/Save et Implicits Arguments)	herbelin	2002-04-17
*	Amélioration des messages d'erreurs concernant l'inférence des implicites	herbelin	2002-04-10
*	- modifs de la condition de garde pour mieux tenir compte des raisonnements	barras	2002-04-02
*	code mort dans tactinterp; plus de Debug On/Off dans Correctness	filliatr	2002-02-21
*	- Reforme de la gestion des args recursifs (via arbres reguliers)	barras	2002-02-14
*	affichages avec prterm_env et non prterm; deb_print pour vraiment ne rien fai...	filliatr	2002-02-08
*	petit nettoyage de kernel/inductive	barras	2002-02-07
*	Zinv -> Zopp	filliatr	2002-01-21
*	Corrections post contournement des streams avec ++	herbelin	2001-12-19
*	le save de Correctness faisant assert false	barras	2001-12-17
*	compat ocaml 3.03	filliatr	2001-12-13
*	nouvel algo de conversion plus uniforme	barras	2001-11-29
*	Fusion de declare/add_constant, declare/add_parameter et add_discharged_constant	herbelin	2001-11-20