coq - The formal proof system

Age	Commit message (Expand)	Author
2000-11-20	Ajout d'une Nametab et d'un flag export aux ClosedSection; on applique export...	herbelin
2000-11-15	methode export	filliatr
2000-11-10	Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...	herbelin
2000-11-10	Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...	herbelin
2000-11-09	Renommage canonique SectionLocalDecl -> SectionLocalAssum	herbelin
2000-11-08	nouveau load path	filliatr
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-11-02	correction Abstract (et make world passe!)	filliatr
2000-11-02	suppression des (* open Generic *)	filliatr
2000-10-31	- simplification Makefile (compilation des fichiers .ml'; pas encore parfait	filliatr
2000-10-30	Pour le Require Export (temporaire)	delahaye
2000-10-26	Require Export recursifs	filliatr
2000-10-25	Bug pop_path_prefix : List.rev manquant	herbelin
2000-10-23	L'état implicite des définitions survivant au discharge redevient celui du ...	herbelin
2000-10-23	module_segment et module_filename	filliatr
2000-10-18	Simplifications autour de typed_type (renommé types par analogie avec sorts)...	herbelin
2000-10-18	Renommage canonique :	herbelin
2000-10-11	Prise en compte de l'environnement dans le calcul des implicites	herbelin
2000-10-11	Prise en compte de Let dans build_dependent_inductive	herbelin
2000-10-06	Correction incompatibilites dans la fn des types des inductifs	herbelin
2000-10-06	correction bug univers (dummy_univ)	filliatr
2000-10-01	Renommage AppL en App	herbelin
2000-10-01	Chasse aux de-cast inutiles	herbelin
2000-10-01	Disparition du type oper mais nouveau type global_reference	herbelin
2000-09-15	On laisse les LetIn dans les types des constructeurs et des éliminations	herbelin
2000-09-14	Abstraction de constr	herbelin
2000-09-14	Intégré à Tacred	herbelin
2000-09-12	Modification mkAppL; abstraction via kind_of_term; changement dans Reduction	herbelin
2000-09-10	Correction pour make doc	herbelin
2000-09-10	Suppression de Abst	herbelin
2000-09-10	Ajout d'un LetIn primitif.	herbelin
2000-09-10	Ajout d'un LetIn primitif.	herbelin
2000-09-10	Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. Abstract...	herbelin
2000-09-10	Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path	herbelin
2000-08-21	Nametab.init - bug corrected	coq
2000-07-25	retablissement make doc et make minicoq	filliatr
2000-07-24	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin
2000-07-01	Précalcul de la forme canonique des constructeurs et arités pour traiter le...	herbelin
2000-06-21	bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> .vo...	filliatr
2000-06-01	Mise en place d'un choix constr/typed_type en remplacement de certains Cast	herbelin
2000-05-31	Nettoyage de Generic	herbelin
2000-05-31	Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeurs	herbelin
2000-05-31	Amélioration capture des erreurs	herbelin
2000-05-22	Bugs d'index d'inductive	herbelin
2000-05-22	suppression de l'env/sigma dans les fonctions de reduction beta et iota seuls	herbelin
2000-05-22	Suite restructuration inductifs; changement nom module Constant en Declarations	herbelin
2000-05-18	Effets de bords suite à la restructuration des inductives (cf Inductive)	herbelin
2000-05-18	Adaptation pour nouveaux inductifs (cf Inductive)	herbelin