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.ml | |
| 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.ml')
| -rw-r--r-- | library/global.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/library/global.ml b/library/global.ml index d4ad97a8c..6ad414339 100644 --- a/library/global.ml +++ b/library/global.ml @@ -73,15 +73,15 @@ let add_constraints c = global_env := add_constraints c !global_env let set_engagement c = global_env := set_engagement c !global_env -let start_module id params mtyo = +let start_module id params = let l = label_of_id id in - let mp,newenv = start_module l params mtyo !global_env in + let mp,newenv = start_module l params !global_env in global_env := newenv; mp -let end_module id = +let end_module id mtyo = let l = label_of_id id in - let mp,newenv = end_module l !global_env in + let mp,newenv = end_module l mtyo !global_env in global_env := newenv; mp |