coq - The formal proof system

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