coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Traduction des noms v7 de Z en noms v8	herbelin	2005-12-25
*	Traduction des noms v7 de R en noms v8	herbelin	2005-12-25
*	Utilisation de -notop pour imposer l'absence de module toplevel	herbelin	2005-12-25
*	maj	coq	2005-12-24
*	Changement de stratégie vis à vis du positionnement du module Top en mode b...	herbelin	2005-12-24
*	Tentative de réparation du bug #1025: it seems like that a casted module sho...	herbelin	2005-12-24
*	maj	coq	2005-12-23
*	* empty log message *	herbelin	2005-12-23
*	Débranchement des parseurs de syntaxe v7	herbelin	2005-12-23
*	Simplifification de vernac_expr li l'abandon du traducteur	herbelin	2005-12-23
*	MAJ restructuration constrintern.ml	herbelin	2005-12-23
*	Vérification qu'un module est ouvert avant d'insérer une déclaration nomm�...	herbelin	2005-12-23
*	Correction printer des Tactic Notation	herbelin	2005-12-23
*	Correction pr_module pour traducteur	herbelin	2005-12-23
*	Test printing of Tactic Notation which was broken until dec 2005	herbelin	2005-12-23
*	maj	coq	2005-12-22
*	Abandon tests syntaxe v7 (correction)	herbelin	2005-12-22
*	Contrepartie de la suppression des boites automatiques dans format	herbelin	2005-12-22
*	option '-top dir' now works also in batch mode (2ème)	herbelin	2005-12-22
*	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin	2005-12-22
*	option '-top dir' now works also in batch mode; it is even necessary to ensur...	herbelin	2005-12-22
*	Double bug de interp_modifiers anciennement caché par un troisième que les ...	herbelin	2005-12-22
*	Correction bugs commit précédent	herbelin	2005-12-22
*	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin	2005-12-21
*	Abandon tests syntaxe v7; ajouts tests modules	herbelin	2005-12-21
*	maj	coq	2005-12-21
*	MAJ syntaxe v7 avant activation en syntaxe v8	herbelin	2005-12-21
*	Activation du test de Refine en v7 pour mémoire avant passage à la v8	herbelin	2005-12-21
*	Anciennement déplacé dans 'output'	herbelin	2005-12-21
*	cf ltac4.v	herbelin	2005-12-21
*	MAJ	herbelin	2005-12-21
*	Divers; restructuration des points d'entrée de Constrintern	herbelin	2005-12-21
*	Prise en compte de l'information que certaines tactiques attendent un type (u...	herbelin	2005-12-21
*	Restructuration des points d'entrée de Pretyping et Constrintern	herbelin	2005-12-21
*	Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...	herbelin	2005-12-21
*	Uniformisation: extension de la suppression d'un casts dans collapse_app à l...	herbelin	2005-12-21
*	maj	coq	2005-12-20
*	Abandon gestion des extensions de syntaxe de la v7 et du traducteur dans meta...	herbelin	2005-12-20
*	maj	coq	2005-12-19
*	Suppression de la mise en boite automatique si format utilisateur	herbelin	2005-12-19
*	maj	coq	2005-12-18
*	L'option -no-vm laisse la place à une option -vm	herbelin	2005-12-18
*	maj	coq	2005-12-17
*	maj	coq	2005-12-17
*	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
*	Orthographe de 'instantiate'	herbelin	2005-12-17
*	maj	coq	2005-12-16
*	amelioration de l'extraction haskell: affichage du type des fonctions, et sup...	letouzey	2005-12-16
*	multiples ameliorations de l'extraction scheme:	letouzey	2005-12-16