aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* SearchPattern et SearchRewriteGravatar filliatr2000-11-24
* - coqc: utilise le meilleur coq possibleGravatar filliatr2000-11-24
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* Informations inutilesGravatar herbelin2000-11-23
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* Bug qualidconstarg (intervient pour Transparent)Gravatar herbelin2000-11-23
* Reparation IsMutConstruct + TransparentGravatar mohring2000-11-23
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* NettoyageGravatar herbelin2000-11-22
* deplacement poly_args; iterateurs sur les segmentsGravatar filliatr2000-11-22
* retablissement de line_oriented_parser pour YvesGravatar filliatr2000-11-22
* Elimination d'un test sur les macrosGravatar delahaye2000-11-21
* implicites manuelsGravatar filliatr2000-11-21
* Begin-End Silent deviennent Set?Unset SilentGravatar mohring2000-11-21
* separation calcul des implicites et declaration des constantes / inductifs / ...Gravatar filliatr2000-11-21
* Petit bug entre close_section'sGravatar herbelin2000-11-20
* Prise en compte des noms qualifiés dans certaines commandesGravatar herbelin2000-11-20
* Prise en compte noms longsGravatar herbelin2000-11-20
* Tables séparées pour chaque type de global; calcul de la Nametab de la sect...Gravatar herbelin2000-11-20
* Ajout erreur GlobalNotFoundGravatar herbelin2000-11-20
* Mieux à sa place dans toplevelGravatar herbelin2000-11-20
* Prise en compte noms longsGravatar herbelin2000-11-20
* Une capsule pour save_module_to dans DischargeGravatar herbelin2000-11-20
* methode exportGravatar filliatr2000-11-15
* Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...Gravatar herbelin2000-11-10
* Renommage canonique SectionLocalDecl -> SectionLocalAssumGravatar herbelin2000-11-09
* nouveau load pathGravatar filliatr2000-11-08
* améliorationGravatar herbelin2000-11-08
* out_variable (Liboject.obj -> ...) distibgue de get_variableGravatar filliatr2000-11-08
* Modification de la table des tactic Definitions pour eviter l'ecritureGravatar mohring2000-11-07
* Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...Gravatar herbelin2000-11-06
* print_idl inlinéGravatar herbelin2000-11-06
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* compilation avec make de Solaris; README et INSTALLGravatar filliatr2000-11-03
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Ajout d'un switch pour le debuggerGravatar delahaye2000-10-30
* g_natsyntax et g_zsyntax maintenant toujours linkesGravatar filliatr2000-10-27
* Meilleur endroit pour déclarer les parseurs de grammaires et joli affichageGravatar herbelin2000-10-24
* Rétablissement compatibilité des implicites (2ème) (mais amélioration)Gravatar herbelin2000-10-23
* Import de Infix au RequireGravatar herbelin2000-10-23
* code mortGravatar herbelin2000-10-23
* L'état implicite des définitions survivant au discharge redevient celui du ...Gravatar herbelin2000-10-23
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Correction bug affichage des infixGravatar herbelin2000-10-16
* Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...Gravatar herbelin2000-10-13
* Hypotheses des ind oubliees dans le dischargeGravatar herbelin2000-10-12
* Message d'erreur bad patternGravatar herbelin2000-10-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 10:32:38 +0000