From 206ce9892fbfc2dbac151fb3479b9a0849461536 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Tue, 2 Feb 2010 15:35:21 +0000
Subject: Small fix on module inclusion.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12706 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index ffe53e505f..dce84ff043 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -106,7 +106,7 @@ let load_constant i ((sp,kn),(_,_,kind)) =
 
 (* Opening means making the name without its module qualification available *)
 let open_constant i ((sp,kn),_) =
-  let con = constant_of_kn kn in
+  let con = Global.constant_of_delta (constant_of_kn kn) in
     Nametab.push (Nametab.Exactly i) sp (ConstRef con)
 
 let cache_constant ((sp,kn),(cdt,dhyps,kind)) =
-- 
cgit v1.2.3