coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	corrections de bug de la reduction	barras	2001-03-08
*	compare_constr independent du groupement des applications.	barras	2001-03-08
*	réparation (?) discharge axiome	filliatr	2001-03-06
*	Re-Déplacement extended_rel_list	herbelin	2001-03-05
*	Déplacement de qualid dans Nametab, hors du noyau	herbelin	2001-03-01
*	nouvelle implantation de la reduction	barras	2001-03-01
*	retire profile	mohring	2001-02-28
*	Changement de subst_meta	mohring	2001-02-28
*	ident au lieu de string pour le nom de base de qualid	herbelin	2001-02-16
*	Mise en place d'un système optionnel de discharge immédiat; prise en compte...	herbelin	2001-02-14
*	simplification du make depend; fonctions de stat. util. memoire dans certains...	filliatr	2001-02-08
*	Chgt signature de type_of_existential	herbelin	2001-02-07
*	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin	2001-02-07
*	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr	2001-01-31
*	Ajout d'espace dans les règles d'affichage des infix si des lettres figurent...	herbelin	2001-01-31
*	make doc	herbelin	2001-01-27
*	Ajout alias mutual_inductive_path = section_path	herbelin	2001-01-27
*	Ajout global_vars_decl	herbelin	2001-01-24
*	Doc	herbelin	2001-01-24
*	Déplacement du type stack de Reduction vers Closure et utilisation pour acc�...	herbelin	2000-12-26
*	Alias variable_path	herbelin	2000-12-25
*	Bug mauvais environnement dans le test d'eta-conversion	herbelin	2000-12-20
*	Export de it_mkProd_or_LetIn_name et it_mkLambda_or_LetIn_name	herbelin	2000-12-18
*	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-15
*	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-14
*	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