diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-15 15:30:04 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-15 15:30:04 +0000 |
| commit | a4e3d24ed286084592897b2c6fa3044e68e0206e (patch) | |
| tree | b7034615c897531a324793945324dd6b0e4a6c63 /library/global.mli | |
| parent | cb9e98ab7a57ab2bcf874a2c8bb58cbb94e5be87 (diff) | |
Inversion de l'ordre de chargement des objets logiques et non logiques
à la déclaration des paramètres de foncteurs (problème de
synchronisation révélé par bug #1118, apparu suite à l'appel de
lookup_mind par load_struct, suite au passage à un discharge local)
Les objets non logiques sont maintenant chargés après car ils peuvent
dépendre d'objets logiques. Et comme les objets non logiques
(p.ex. l'import récursif de modules dans la nametab) sont nécessaires
au typage de l'éventuelle contrainte de module, on reporte la gestion
de la contrainte au moment du end_module (on aurait peut-être pu faire
plus fin et extraire dans do_module la partie purement module, mais
après tout le report de la contrainte de type dans le end_module ne
semble pas génante).
À la date d'aujourd'hui, le bug #1118 reste toutefois ouvert avec les
définitions de module non interactives.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8721 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/global.mli')
| -rw-r--r-- | library/global.mli | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/library/global.mli b/library/global.mli index 579882498..af6ec6ae9 100644 --- a/library/global.mli +++ b/library/global.mli @@ -64,12 +64,10 @@ val set_engagement : engagement -> unit of the started module / module type *) val start_module : - identifier -> (mod_bound_id * module_type_entry) list - -> module_type_entry option - -> module_path + identifier -> (mod_bound_id * module_type_entry) list -> module_path val end_module : - identifier -> module_path + identifier -> module_type_entry option -> module_path val start_modtype : identifier -> (mod_bound_id * module_type_entry) list |