coq - The formal proof system

Age	Commit message (Expand)	Author
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-04-16	Déplacement/renommage de Class.stre_max en Declare.strength_min	herbelin
2002-02-12	Raffinement library_part	herbelin
2002-02-12	Ajout library_part	herbelin
2001-11-20	Fusion de declare/add_constant, declare/add_parameter et add_discharged_constant	herbelin
2001-11-19	Mise en place d'une méthode directe pour indiquer le type des déclarations ...	herbelin
2001-11-05	GROS COMMIT:	barras
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-09-20	Transparent	barras
2001-09-20	Nettoyage des commentaires	herbelin
2001-09-19	Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...	herbelin
2001-09-19	Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et le...	herbelin
2001-09-18	Mise en place de noms contenant la section pour Fact et Remark	herbelin
2001-09-10	Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...	herbelin
2001-09-09	Légère modification lookup_eliminator	herbelin
2001-09-09	Mécanisme pour faire remonter les contraintes de typage sur les variables de...	herbelin
2001-08-10	Parsing	herbelin
2001-08-01	Ajout make_elimination_ident	herbelin
2001-05-16	Correction d'un commentaire erroné.	clrenard
2001-03-15	entetes	filliatr
2001-03-01	Déplacement de qualid dans Nametab, hors du noyau	herbelin
2001-02-14	Mise en place d'un système optionnel de discharge immédiat; prise en compte...	herbelin
2001-01-27	Ajout alias mutual_inductive_path = section_path	herbelin
2001-01-24	Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...	herbelin
2001-01-24	Réorganisation suite ajout de constantes locales dans les Records	herbelin
2000-12-29	Ajout du Let pour le langage de tactiques	delahaye
2000-12-25	find_section_variable : un traducteur id -> sp pour variables de section; var...	herbelin
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-12-04	caractere opaque des constantes repris en compte	filliatr
2000-11-26	Nettoyage	herbelin
2000-11-26	Prise en compte de noms absolus dans la nametab + nettoyage	herbelin
2000-11-22	Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...	herbelin
2000-11-21	separation calcul des implicites et declaration des constantes / inductifs / ...	filliatr
2000-11-20	Nouveaux points d'accès pour les noms qualifiés	herbelin
2000-11-09	Renommage canonique SectionLocalDecl -> SectionLocalAssum	herbelin
2000-11-08	out_variable (Liboject.obj -> ...) distibgue de get_variable	filliatr
2000-11-06	Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...	herbelin
2000-11-06	nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...	filliatr
2000-10-18	Renommage canonique :	herbelin
2000-10-01	Disparition du type oper mais nouveau type global_reference	herbelin
2000-07-24	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin
2000-05-22	Suite restructuration inductifs; changement nom module Constant en Declarations	herbelin
2000-04-28	portage Omega (code seulement)	filliatr
2000-04-21	discharge des axiomes	filliatr
1999-12-15	Nouveaux types 'constructor' et 'inductive' dans Term;	herbelin
1999-12-12	modules	filliatr
1999-12-08	deplacement de Discharge dans toplevel	filliatr
1999-12-06	declarations eliminations / debuggae inductifs (debut)	filliatr
1999-12-03	- global_reference traite des variables	filliatr