coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	open superflu	herbelin	2003-09-12
*	Ajout construction If primitive dans constr_expr et rawconstr	herbelin	2003-09-09
*	Mise en place possibilité de définitions locales dans les paramètres des i...	herbelin	2003-09-06
*	Bug détypage du fix	herbelin	2003-08-12
*	Nouvelle mouture du traducteur v7->v8	herbelin	2003-08-11
*	Factorisation de detype_case pour utilisation par l'afficheur de pattern	herbelin	2003-06-10
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Affichage des Fix contenant des Let dans leur context (ce que la tactique Fix...	herbelin	2003-04-27
*	Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)	herbelin	2003-03-29
*	* empty log message *	barras	2003-03-12
*	Bug affichage let destructurant	herbelin	2003-02-02
*	Problème de désynchronisation des variables du type et du corps d'un point-...	herbelin	2003-01-15
*	Affinement affichage	herbelin	2002-12-21
*	apres correction du probleme de Global.env, retour du mis_constr_nargs_env	letouzey	2002-12-19
*	ma bidouille marche pas...	letouzey	2002-12-17
*	correction (temporaire ?) d'un probleme de Printer.prterm_env utilisant quand...	letouzey	2002-12-13
*	Problèmes et améliorations divers affichage	herbelin	2002-12-09
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Utilisation d'une construction spéciale SECVAR pour gérer la	herbelin	2002-05-14
*	- Reforme de la gestion des args recursifs (via arbres reguliers)	barras	2002-02-14
*	substitution et pattern modulo let	barras	2002-02-11
*	petit nettoyage de kernel/inductive	barras	2002-02-07
*	compat ocaml 3.03	filliatr	2001-12-13
*	Bug nommage des fonctions définies par récursion mutuelle	herbelin	2001-11-19
*	Re-installation de l'affichage des globaux par des noms courts	herbelin	2001-11-19
*	GROS COMMIT:	barras	2001-11-05
*	Reorganisation de Goption. Passage des options l'utilisant en synchrone	letouzey	2001-10-30
*	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin	2001-10-11
*	Suppression des arguments sur les constantes, inductifs et constructeurs	barras	2001-10-09
*	Bug d'affichage du prédicat, bug d'affichage des clauses en présence de dé...	herbelin	2001-10-03
*	Réparation des options Set Printing and co	herbelin	2001-09-21
*	erreur de pretty-print lors de l'affichage de termes avec de Bruijn non lies	barras	2001-09-04
*	Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...	herbelin	2001-07-21
*	Facilites pour le debogguage des univers.	coq	2001-05-29
*	Changement de la structure des points fixes	barras	2001-05-03
*	entetes	filliatr	2001-03-15
*	Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation	herbelin	2001-03-11
*	nouvelle implantation de la reduction	barras	2001-03-01
*	uniformisation avec constr des lieurs dans rawterm/pattern	herbelin	2001-02-14
*	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin	2001-02-07
*	Prise en compte du let-in dans lookup_*_as_renamed	herbelin	2001-01-30
*	Bugs prise en compte du prédicat dans le Cases; le prédicat du Cases devien...	herbelin	2000-12-14
*	Utilisation de global_reference dans rawconstr; blindage pour quand appelé d...	herbelin	2000-11-20
*	suppression des (* open Generic *)	filliatr	2000-11-02
*	Renommage canonique :	herbelin	2000-10-18
*	Bug affichage du nom des letin	herbelin	2000-10-11
*	Renommage AppL en App	herbelin	2000-10-01
*	Abstraction de constr	herbelin	2000-09-14