diff options
| author | herbelin | 2006-04-15 15:30:04 +0000 |
|---|---|---|
| committer | herbelin | 2006-04-15 15:30:04 +0000 |
| commit | a4e3d24ed286084592897b2c6fa3044e68e0206e (patch) | |
| tree | b7034615c897531a324793945324dd6b0e4a6c63 /kernel/modops.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 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index b20e7259d5..166b230077 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -41,7 +41,7 @@ let error_incompatible_labels l l' = error ("Opening and closing labels are not the same: " ^string_of_label l^" <> "^string_of_label l'^" !") -let error_result_must_be_signature mtb = +let error_result_must_be_signature () = error "The result module type must be a signature" let error_signature_expected mtb = |