| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2000-11-23 | Ajout push_rels_assum | herbelin |
| 2000-11-23 | Bug qualidconstarg (intervient pour Transparent) | herbelin |
| 2000-11-23 | Reparation IsMutConstruct + Transparent | mohring |
| 2000-11-22 | Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's... | herbelin |
| 2000-11-22 | Nettoyage | herbelin |
| 2000-11-22 | deplacement poly_args; iterateurs sur les segments | filliatr |
| 2000-11-22 | Reparation bug mutuels ind | mohring |
| 2000-11-22 | retablissement de line_oriented_parser pour Yves | filliatr |
| 2000-11-22 | des proofs/macros qui trainaient dans le Makefile et le .depend | filliatr |
| 2000-11-21 | Tout est deja traite dans Tacinterp | delahaye |
| 2000-11-21 | Elimination d'un test sur les macros | delahaye |
| 2000-11-21 | Traitement du pretty-print des Redexp | delahaye |
