coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Lazy manuelles dans le code	coq	2002-10-07
*	correcting the treatment of many tactics that use quant_hyp in file xlate.ml	bertot	2002-10-06
*	Lazy experimentale temporaire...	coq	2002-10-05
*	Re-introduce the treatement of Tacticals that Hugo had already done in	bertot	2002-10-04
*	Previous version did compile but did not make it possible to actually run	bertot	2002-10-03
*	Omega can now elim hyps of type False. Therefore, it knows how to deal	courant	2002-10-02
*	Adding the congruence closure tactics (CC and CCsolve).	corbinea	2002-10-01
*	Complétion filtrage	herbelin	2002-09-29
*	Un peu (plus) d'ordre dans Nametab...	coq	2002-09-24
*	suite chgt liés aux modules	letouzey	2002-09-24
*	portage Correctness (substitutivité pour les modules)	filliatr	2002-09-19
*	retablissement de Correctness (pas encore teste' cependant)	filliatr	2002-09-18
*	Suppression automatique du corps des définitions locales opaques dans	herbelin	2002-08-17
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	reparation d'un bug (dummy_lams -> anonym_lams) + chgmt structutr d'un ml_type	letouzey	2002-07-24
*	reparation temporaire(?) a coup de MLdummy'	letouzey	2002-07-17
*	maj	letouzey	2002-07-16
*	Pour ocamlweb	letouzey	2002-07-16
*	Souci avec example fbidon...	letouzey	2002-07-16
*	petit bug lors du passage d'hugo	letouzey	2002-07-16
*	Gros Remaniement Extraction:	letouzey	2002-07-16
*	Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour	herbelin	2002-07-11
*	Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulement	filliatr	2002-06-21
*	ZArith_base, Zbool, Bool_nat	filliatr	2002-06-20
*	Reparation de ring pour les setoides	clrenard	2002-06-19
*	ProgWf -> Zwf	filliatr	2002-06-19
*	deplacement contrib/correctness/ProgWf -> theories/ZArith/Zwf	filliatr	2002-06-19
*	extraction vers scheme	letouzey	2002-06-07
*	Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...	herbelin	2002-06-05
*	Intgration uniforme de coercions dans les dclarations (Variable and co) et re...	herbelin	2002-06-03
*	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
*	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
*	- abstract_sum_scalar, plus_sum_scalar and minus_sum_scalar were bogus	barras	2002-05-15
*	petit bug dans les noms de fichiers	letouzey	2002-04-24
*	un thm de plus dans Zdiv; un retour chariot apres un message de la tactique F...	filliatr	2002-04-19
*	* empty log message *	letouzey	2002-04-18
*	jLogic.mli remplace par jolic.mli	herbelin	2002-04-17
*	Uniformisation (Qed/Save et Implicits Arguments)	herbelin	2002-04-17
*	Refine the procedure that generalizes context to current goal.	huang	2002-04-15
*	maj doc extraction dans repertoire contrib/extraction	letouzey	2002-04-15
*	maj test des reals	letouzey	2002-04-12
*	petit bug avec dummy_lams	letouzey	2002-04-12
*	Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.ml	herbelin	2002-04-11
*	Amélioration des messages d'erreurs concernant l'inférence des implicites	herbelin	2002-04-10
*	extraction.ml	letouzey	2002-04-08
*	babioles de renommages	letouzey	2002-04-08