aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2000-11-27Affichage des définitions localesherbelin
2000-11-27Ajout map_constr_with_full_binders et strong pour Simplherbelin
2000-11-27Changement du parseur par défaut dans Syntaxherbelin
2000-11-27Généralisation de constant_opt_value en reference_opt_valueherbelin
2000-11-27Branchement du mécanisme d'instantiation des Evar en présence de définitio...herbelin
2000-11-27Prise en compte des let-in dans les fonctions de réduction pour les tactiquesherbelin
2000-11-27Bug dans le calcul des dépendances dans add_discharged_constantherbelin
2000-11-26Nettoyageherbelin
2000-11-26Appel des constantes globaux par des noms absolusherbelin
2000-11-26Le nouvel Induction s'appelle NewInductionherbelin
2000-11-26MAJherbelin
2000-11-26Prise en compte qualidherbelin
2000-11-26Restruration autour de qualidargherbelin
2000-11-26Calcul du chemin optimal dans qualid_of_globalherbelin
2000-11-26Distinction claire entre Induction (nom interne : raw_induct) et le nouvel in...herbelin
2000-11-26Prise en compte noms longs dans divers fonctions de Printherbelin
2000-11-26Prise en compte de noms absolus dans la nametab + nettoyageherbelin
2000-11-26Prise en compte de noms absolus dans la nametabherbelin
2000-11-26Remplacement de certains sp_of_id par des locateherbelin
2000-11-26sp au lieu de id dans END-SECTIONherbelin
2000-11-24MAJherbelin
2000-11-24Bug relocation des hypothèses quand les contextes de définitions et d'utili...herbelin
2000-11-24Réorganisation autour de globalize_constrherbelin
2000-11-24Nettoyageherbelin
2000-11-24Ajout d'un .:/opt/kde/bin:/home/herbelin/bin:/bin:/sbin:/usr/bin:/usr/etc:/us...herbelin
2000-11-24Paramètrage de ocamldebug-v7 par configure à partir d'un 'template'herbelin
2000-11-24MAJfilliatr
2000-11-24Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametabfilliatr
2000-11-24Ajout BEST partout a coqcfilliatr
2000-11-24certains effets disparaissent a la sortie des sections, d'autres non (selon S...filliatr
2000-11-24resolution implicites dans produits (bug)filliatr
2000-11-24SearchPattern et SearchRewritefilliatr
2000-11-24MAJherbelin
2000-11-24synchronisation Requirefilliatr
2000-11-24- coqc: utilise le meilleur coq possiblefilliatr
2000-11-24Petite simplif due au nouveau Tautodelahaye
2000-11-24Nouveau choix pour l'intros initialdelahaye
2000-11-23Ajout d'une syntaxe pour Reals.mayero
2000-11-23On n'introduit que des produits non dependantsdelahaye
2000-11-23Correction d'un bug lorsque des Variables sont clearees dans le but courantdelahaye
2000-11-23Affichage des QUALIDherbelin
2000-11-23Simplification de l'accès aux globauxherbelin
2000-11-23Search réparéfilliatr
2000-11-23MAJherbelin
2000-11-23print_id, print_sp -> pr_id, pr_spherbelin
2000-11-23Affichage des paths avec des '.', print_id -> pr_id, print_sp -> pr_spherbelin
2000-11-23id_of_global devient sp_of_globalherbelin
2000-11-23Fonction qualid_of_global pour affichage des paths avec des '.'herbelin
2000-11-23Affichage des paths avec des '.', 2eme; prise en compte qualidherbelin
2000-11-23Informations inutilesherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 21:55:08 +0000