From a4e3d24ed286084592897b2c6fa3044e68e0206e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 15 Apr 2006 15:30:04 +0000
Subject: 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
---
 kernel/modops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/modops.ml')

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 =
-- 
cgit v1.2.3