| Age | Commit message (Expand) | Author |
|---|
| 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-26 | Nettoyage | herbelin |
| 2000-11-26 | Appel des constantes globaux par des noms absolus | herbelin |
| 2000-11-26 | Le nouvel Induction s'appelle NewInduction | herbelin |
| 2000-11-26 | MAJ | herbelin |
| 2000-11-26 | Prise en compte qualid | herbelin |
| 2000-11-26 | Restruration autour de qualidarg | herbelin |
| 2000-11-26 | Calcul du chemin optimal dans qualid_of_global | herbelin |
| 2000-11-26 | Distinction claire entre Induction (nom interne : raw_induct) et le nouvel in... | herbelin |
| 2000-11-26 | Prise en compte noms longs dans divers fonctions de Print | herbelin |
| 2000-11-26 | Prise en compte de noms absolus dans la nametab + nettoyage | herbelin |
| 2000-11-26 | Prise en compte de noms absolus dans la nametab | herbelin |
| 2000-11-26 | Remplacement de certains sp_of_id par des locate | herbelin |
| 2000-11-26 | sp au lieu de id dans END-SECTION | herbelin |
| 2000-11-24 | MAJ | herbelin |
| 2000-11-24 | Bug relocation des hypothèses quand les contextes de définitions et d'utili... | herbelin |
| 2000-11-24 | Réorganisation autour de globalize_constr | herbelin |
| 2000-11-24 | Nettoyage | herbelin |
| 2000-11-24 | Ajout d'un .:/opt/kde/bin:/home/herbelin/bin:/bin:/sbin:/usr/bin:/usr/etc:/us... | herbelin |
| 2000-11-24 | Paramètrage de ocamldebug-v7 par configure à partir d'un 'template' | herbelin |
| 2000-11-24 | MAJ | filliatr |
| 2000-11-24 | Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametab | filliatr |
| 2000-11-24 | Ajout BEST partout a coqc | filliatr |
| 2000-11-24 | certains effets disparaissent a la sortie des sections, d'autres non (selon S... | filliatr |
| 2000-11-24 | resolution implicites dans produits (bug) | filliatr |
| 2000-11-24 | SearchPattern et SearchRewrite | filliatr |
| 2000-11-24 | MAJ | herbelin |
| 2000-11-24 | synchronisation Require | filliatr |
| 2000-11-24 | - coqc: utilise le meilleur coq possible | filliatr |
| 2000-11-24 | Petite simplif due au nouveau Tauto | delahaye |
| 2000-11-24 | Nouveau choix pour l'intros initial | delahaye |
| 2000-11-23 | Ajout d'une syntaxe pour Reals. | mayero |
| 2000-11-23 | On n'introduit que des produits non dependants | delahaye |
| 2000-11-23 | Correction d'un bug lorsque des Variables sont clearees dans le but courant | delahaye |
| 2000-11-23 | Affichage des QUALID | herbelin |
| 2000-11-23 | Simplification de l'accès aux globaux | herbelin |
| 2000-11-23 | Search réparé | filliatr |
| 2000-11-23 | MAJ | herbelin |
| 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 | id_of_global devient sp_of_global | herbelin |
| 2000-11-23 | Fonction qualid_of_global pour affichage des paths avec des '.' | herbelin |
| 2000-11-23 | Affichage des paths avec des '.', 2eme; prise en compte qualid | herbelin |
| 2000-11-23 | Informations inutiles | herbelin |
| 2000-11-23 | Affichage des paths avec des '.'; print_id, print_sp -> pr_id, pr_sp; | herbelin |
| 2000-11-23 | print_id, print_sp -> pr_id, pr_sp | herbelin |
