coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	GROS COMMIT:	barras	2001-11-05
*	Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR	delahaye	2001-10-23
*	Abstraction de l'immplementation de dirpath et implementation dans l'autre se...	herbelin	2001-10-17
*	reparation	filliatr	2001-10-12
*	Suppression des arguments sur les constantes, inductifs et constructeurs	barras	2001-10-09
*	Parsing	herbelin	2001-08-10
*	correction d'un bug de Correctness (pour Y Bertot)	filliatr	2001-06-27
*	nettoyage	filliatr	2001-05-28
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23
*	Modification afin de permettre plusieurs modifs successives d'une commande	clrenard	2001-05-18
*	message 'is defined' seulement en mode verbose	filliatr	2001-05-10
*	expansion des constr purs	filliatr	2001-04-23
*	nettoyage	filliatr	2001-04-20
*	remplace Zarith par ZArith	mohring	2001-04-19
*	documentation automatique de la bibliothèque standard	filliatr	2001-04-11
*	réparation d'un bug de Correctness: whd_programs ne doit pas réduire les te...	filliatr	2001-04-11
*	portage exemples Correctness; changement du nom de pred_of_minus dans coq_omega	filliatr	2001-04-10
*	réparation Correctness; options Extraction (changement de syntaxe)	filliatr	2001-04-10
*	exemples Correctness	filliatr	2001-04-09
*	branchement extraction en standard (pas de Require)	filliatr	2001-04-09
*	mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4	filliatr	2001-04-05
*	renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...	filliatr	2001-04-04
*	deux fichiers (past et ptype) uniquement sous forme de .mli	filliatr	2001-04-04
*	psyntax.ml4 sous CVS	filliatr	2001-04-03