coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Nouveau long long avec Coq en tête	herbelin	2000-11-29
*	Enregistrement des racines de la bibliothèque	herbelin	2000-11-29
*	Ajout d'un alias à add_path, rec_add_path et all_subdirs pour associer un ch...	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
*	Now also inner-types are exported.	sacerdot	2000-11-29
*	Hack pour contourner CVS en local dans la recherche rcursive de load_path	herbelin	2000-11-28
*	Remplacement des add_include par add_rec_include pour avoir le repertoire dan...	herbelin	2000-11-28
*	Les variables doivent persister dans les vo pour HELM	herbelin	2000-11-28
*	Code clean-up due to the new usage of longer names in Coq.	sacerdot	2000-11-28
*	Prise en compte du repertoire dans le section path; utilisation de dirpath po...	herbelin	2000-11-28
*	Ajout des Fix et CoFix dans les patterns	delahaye	2000-11-28
*	Added -R inclusion to fix compilation in not-local configuration.	sacerdot	2000-11-28
*	-I inutiles pour coqc et utilisation de -R theories (pour garder trace des no...	herbelin	2000-11-28
*	Elimination du '	delahaye	2000-11-28
*	Elimination du '	delahaye	2000-11-28
*	Un == non reconnu sous alpha	delahaye	2000-11-28
*	Rajout de PolyListSyntax aussi dans Makefile	herbelin	2000-11-28
*	Distinction local/global	herbelin	2000-11-27
*	Bug affichage inductifs	herbelin	2000-11-27
*	Xml contrib retached	sacerdot	2000-11-27
*	Many improvements. Xml contrib retached to the V7.	sacerdot	2000-11-27
*	uniformisation messages d'erreur	filliatr	2000-11-27
*	load_module / open_module un tantinet plus rapides	filliatr	2000-11-27
*	Faut-il mettre la réduction let-in dans la réduction unfold ?	herbelin	2000-11-27
*	Remettre une section dans fast_integer pour contourner un bug de définition ...	herbelin	2000-11-27
*	La bonne modif des Unfold	herbelin	2000-11-27
*	MAJ	herbelin	2000-11-27
*	Bug dans find_common_hyps_then_abstract en présence de défs locales	herbelin	2000-11-27
*	La table de pré-évaluation des constantes ne doit pas persister au discharge	herbelin	2000-11-27
*	Bug extract_instance en présence de défs locales	herbelin	2000-11-27
*	Prise en compte des définitions locales	herbelin	2000-11-27
*	Prise en compte des implicites de locaux à l'affichage	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
*	Suppression de Unfold inutile et maintenant échouant	herbelin	2000-11-27
*	Prise en compte des let-in dans les fonctions de réduction pour les tactiques	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
*	Branchement des Local sur des SectionLocalDef	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
*	Affichage des définitions locales	herbelin	2000-11-27
*	Ajout map_constr_with_full_binders et strong pour Simpl	herbelin	2000-11-27
*	Changement du parseur par défaut dans Syntax	herbelin	2000-11-27
*	Généralisation de constant_opt_value en reference_opt_value	herbelin	2000-11-27
*	Branchement du mécanisme d'instantiation des Evar en présence de définitio...	herbelin	2000-11-27
*	Prise en compte des let-in dans les fonctions de réduction pour les tactiques	herbelin	2000-11-27
*	Bug dans le calcul des dépendances dans add_discharged_constant	herbelin	2000-11-27
*	Nettoyage	herbelin	2000-11-26
*	Appel des constantes globaux par des noms absolus	herbelin	2000-11-26