Déclaration des record au chargement (ce n'est pas une question de visibilité mais d'interprétation au niveau global)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5637 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 1 deletions

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 03028dcf35..e2e574d7f7 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -64,7 +64,7 @@ let subst_structure (_,subst,((kn,i),struc as obj)) =
 let (inStruc,outStruc) =
   declare_object {(default_object "STRUCTURE") with 
                     cache_function = cache_structure;
-		    open_function = (fun i o -> if i=1 then cache_structure o);
+		    load_function = (fun _ o -> cache_structure o);
                     subst_function = subst_structure;
 		    classify_function = (fun (_,x) -> Substitute x);
 		    export_function = (function x -> Some x)  }