aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* synchronisation RequireGravatar filliatr2000-11-24
* Fonction qualid_of_global pour affichage des paths avec des '.'Gravatar herbelin2000-11-23
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* deplacement poly_args; iterateurs sur les segmentsGravatar filliatr2000-11-22
* Reparation bug mutuels indGravatar mohring2000-11-22
* reset_name: try / with juste autour de find_entry_p (=> propage lesGravatar filliatr2000-11-21
* ajout d'un frozen_state après la fermeture d'une section (sinon bug !)Gravatar filliatr2000-11-21
* implicites manuelsGravatar filliatr2000-11-21
* correction bug ResetGravatar filliatr2000-11-21
* separation calcul des implicites et declaration des constantes / inductifs / ...Gravatar filliatr2000-11-21
* Petit bug entre close_section'sGravatar herbelin2000-11-20
* Ajout implicits_of_global + accès par noms longsGravatar herbelin2000-11-20
* Open est maintenant géré par NametabGravatar herbelin2000-11-20
* Nouveaux points d'accès pour les noms qualifiésGravatar herbelin2000-11-20
* Nouvelle structure arborescente à la Nametab pour prendre en compte les noms...Gravatar herbelin2000-11-20
* Ajout d'une Nametab et d'un flag export aux ClosedSection; on applique export...Gravatar 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
* 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
* out_variable (Liboject.obj -> ...) distibgue de get_variableGravatar filliatr2000-11-08
* Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...Gravatar herbelin2000-11-06
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* - simplification Makefile (compilation des fichiers .ml'; pas encore parfaitGravatar filliatr2000-10-31
* Pour le Require Export (temporaire)Gravatar delahaye2000-10-30
* Require Export recursifsGravatar filliatr2000-10-26
* Bug pop_path_prefix : List.rev manquantGravatar herbelin2000-10-25
* L'état implicite des définitions survivant au discharge redevient celui du ...Gravatar herbelin2000-10-23
* module_segment et module_filenameGravatar filliatr2000-10-23
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Prise en compte de l'environnement dans le calcul des implicitesGravatar herbelin2000-10-11
* Prise en compte de Let dans build_dependent_inductiveGravatar herbelin2000-10-11
* Correction incompatibilites dans la fn des types des inductifsGravatar herbelin2000-10-06
* correction bug univers (dummy_univ)Gravatar filliatr2000-10-06
* Renommage AppL en AppGravatar herbelin2000-10-01
* Chasse aux de-cast inutilesGravatar herbelin2000-10-01
* Disparition du type oper mais nouveau type global_referenceGravatar herbelin2000-10-01
* On laisse les LetIn dans les types des constructeurs et des éliminationsGravatar herbelin2000-09-15
* Abstraction de constrGravatar herbelin2000-09-14
* Intégré à TacredGravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 14:01:42 +0000