coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12
*	Reparation conditions de positivites inductifs, echange dans add_entry	mohring	2000-12-06
*	Mini-nettoyage noms longs	herbelin	2000-12-05
*	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-29
*	Prise en compte du repertoire dans le section path; utilisation de dirpath po...	herbelin	2000-11-28
*	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-27
*	Prise en compte de noms absolus dans la nametab	herbelin	2000-11-26
*	Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametab	filliatr	2000-11-24
*	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-23
*	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-22
*	Ajout d'une fonction pour recuperer la liste des constantes	delahaye	2000-11-21
*	implicites manuels	filliatr	2000-11-21
*	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-20
*	Code more concernant feu les abstractions	herbelin	2000-11-11
*	Code mort	herbelin	2000-11-10
*	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-07
*	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-06
*	correction Abstract (et make world passe!)	filliatr	2000-11-02
*	suppression des (* open Generic *)	filliatr	2000-11-02
*	- simplification Makefile (compilation des fichiers .ml'; pas encore parfait	filliatr	2000-10-31
*	Suppression cas Cast dans whd_ise et whd_ise1; Suppression du cast au moment ...	herbelin	2000-10-26
*	un espace	herbelin	2000-10-24
*	Bug réduction suite modifs let-in	herbelin	2000-10-24
*	La réduction du Let s'appelle maintenant zeta comme dans le lambda-mu-calcul	herbelin	2000-10-23
*	Simplifications/questions	herbelin	2000-10-23
*	Simplifications autour de typed_type (renommé types par analogie avec sorts)...	herbelin	2000-10-18
*	doc	herbelin	2000-10-18
*	Renommage canonique :	herbelin	2000-10-18
*	Correction pb de globalisation dans print_mutual	herbelin	2000-10-18