coq - The formal proof system

Age	Commit message (Expand)	Author
2000-12-25	Alias variable_path	herbelin
2000-12-20	Bug mauvais environnement dans le test d'eta-conversion	herbelin
2000-12-18	Export de it_mkProd_or_LetIn_name et it_mkLambda_or_LetIn_name	herbelin
2000-12-15	Le bon choix, c'est finalement identifier = string	herbelin
2000-12-15	Mise en place d'un module Ident avec test de l'efficacité quand identifier=s...	herbelin
2000-12-15	- suppression mind_extract_params	filliatr
2000-12-15	Petite réorganisation	herbelin
2000-12-14	Les params d'inductif deviennent en même temps propre à chaque inductif d'u...	herbelin
2000-12-14	Les params d'inductif deviennent en même temps propre à chaque inductif d'u...	herbelin
2000-12-14	MAJ commentaires	herbelin
2000-12-14	Raffinement erreur Wrong Predicate	herbelin
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-12-06	Reparation conditions de positivites inductifs, echange dans add_entry	mohring
2000-12-05	Mini-nettoyage noms longs	herbelin
2000-11-29	Prise en compte de la contrainte de type dans Definition comme étant un cast...	herbelin
2000-11-29	Ajout d'un test pour vérifier qu'on a affaire à un ident	herbelin
2000-11-29	Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypage	herbelin
2000-11-28	Prise en compte du repertoire dans le section path; utilisation de dirpath po...	herbelin
2000-11-27	Faut-il mettre la réduction let-in dans la réduction unfold ?	herbelin
2000-11-27	On déplie les locaux dans les types plutôt que de les quantifier par un Let	herbelin
2000-11-27	Utilisation de Let In pour les constantes locales, prise en compte des Let In...	herbelin
2000-11-27	Bug dans la gestion du contexte en présence de Fix dans le calcul de garde	herbelin
2000-11-27	Prise en compte des let in dans les instances de globaux	herbelin
2000-11-27	Ajout de evaluable_named_decl et evaluable_rel_decl en parallele au evaluable...	herbelin
2000-11-27	Ajout map_constr_with_full_binders et strong pour Simpl	herbelin
2000-11-27	Généralisation de constant_opt_value en reference_opt_value	herbelin
2000-11-27	Bug dans le calcul des dépendances dans add_discharged_constant	herbelin
2000-11-26	Prise en compte de noms absolus dans la nametab	herbelin
2000-11-24	Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametab	filliatr
2000-11-23	print_id, print_sp -> pr_id, pr_sp	herbelin
2000-11-23	Affichage des paths avec des '.', print_id -> pr_id, print_sp -> pr_sp	herbelin
2000-11-23	Ajout push_rels_assum	herbelin
2000-11-23	Reparation IsMutConstruct + Transparent	mohring
2000-11-22	Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...	herbelin
2000-11-22	deplacement poly_args; iterateurs sur les segments	filliatr
2000-11-22	Reparation bug mutuels ind	mohring
2000-11-21	Ajout d'une fonction pour recuperer la liste des constantes	delahaye
2000-11-21	implicites manuels	filliatr
2000-11-20	Tables séparées pour chaque type de global	herbelin
2000-11-20	Ajout sp_of_global; Introduction constant_path = section_path	herbelin
2000-11-20	Introduction constant_path = section_path	herbelin
2000-11-20	Ajout erreur GlobalNotFound	herbelin
2000-11-11	Code more concernant feu les abstractions	herbelin
2000-11-10	Code mort	herbelin
2000-11-07	Modification de la table des tactic Definitions pour eviter l'ecriture	mohring
2000-11-07	Bug sur précédent commit	herbelin
2000-11-07	Nettoyage Names suite	herbelin
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