coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Modification mkAppL; abstraction via kind_of_term; changement dans Reduction	herbelin	2000-09-12
*	Correction pour make doc	herbelin	2000-09-10
*	Suppression de Abst	herbelin	2000-09-10
*	Ajout d'un LetIn primitif.	herbelin	2000-09-10
*	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin	2000-07-24
*	Nettoyage de Generic	herbelin	2000-05-31
*	Modification messages d'erreurs, possibilité de n'importe quel constr dans l...	herbelin	2000-05-26
*	Suite restructuration inductifs; changement nom module Constant en Declarations	herbelin	2000-05-22
*	Effets de bords suite à la restructuration des inductives (cf Inductive)	herbelin	2000-05-18
*	Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'	herbelin	2000-05-02
*	Changement de représentation du contexte des réf dans rawconstr et pattern	herbelin	2000-04-28