coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	correction bug n°191	letouzey	2002-11-25
*	cleanup table.ml + erreur si Extraction Inline sous section	letouzey	2002-11-25
*	Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...	herbelin	2002-11-24
*	Remplacement de Syntactic Definition par Notation	herbelin	2002-11-24
*	Nettoyage	herbelin	2002-11-24
*	remaniement de test_extraction.v	letouzey	2002-11-18
*	typo	herbelin	2002-11-18
*	Complétion du commit précédent	herbelin	2002-11-16
*	Passage à une représentation des fixpoints plus primitive dans constr_expr ...	herbelin	2002-11-15
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	MAJ syntaxe	herbelin	2002-11-14
*	typo	courant	2002-11-13
*	rep why ignore	filliatr	2002-11-12
*	Intégration de la branche mowgli	herbelin	2002-11-05
*	Intégration des modifs de la branche mowgli :	herbelin	2002-11-05
*	cosmetique	letouzey	2002-11-05
*	un bug concernant l'expansion des Map_rec si Map n'est pas ouvert	letouzey	2002-11-04
*	nettoyage et reorganisation	letouzey	2002-11-04
*	maj avec tous les mli	letouzey	2002-11-04
*	Un fichier a utiliser via Drop pour le debug de l'extraction.	letouzey	2002-11-04
*	L'extraction c'est magic cvs -n up	letouzey	2002-10-31
*	Des critères plus fins d'analyse des implicites automatiques; meilleur affic...	herbelin	2002-10-28
*	Clarification changements autour de Remark/Fact/Local	herbelin	2002-10-23
*	Omega échouait à effacer les hypothèses à contenu arithmétique lorsque c...	herbelin	2002-10-23
*	Meilleure lisibilité grâce à tclTHENLIST	herbelin	2002-10-19
*	Réparation bug #180	herbelin	2002-10-19
*	TacCall attend une référence	herbelin	2002-10-14
*	Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'une	herbelin	2002-10-14
*	Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...	herbelin	2002-10-13
*	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