| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2000-11-21 | Ajout d'une fonction pour recuperer la liste des constantes | delahaye |
| 2000-11-21 | Ajout du clean pour tolink.ml | delahaye |
| 2000-11-21 | reset_name: try / with juste autour de find_entry_p (=> propage les | filliatr |
| 2000-11-21 | ln -sf au lieu de ln -s | filliatr |
| 2000-11-21 | ajout d'un frozen_state après la fermeture d'une section (sinon bug !) | filliatr |
| 2000-11-21 | implicites manuels | filliatr |
| 2000-11-21 | PatternMatchingFailure n'etait pas rattrapee | herbelin |
| 2000-11-21 | Nettoyage | herbelin |
| 2000-11-21 | Bugs make_tuple et existS_pattern | herbelin |
| 2000-11-21 | MAJ | herbelin |
| 2000-11-21 | ajout de theories/Wellfounded | filliatr |
| 2000-11-21 | Begin-End Silent deviennent Set?Unset Silent | mohring |
