From 1fd241cdc6a0cee92720230609df17cf97cbc5c8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 28 Nov 2000 17:03:59 +0000
Subject: Les variables doivent persister dans les vo pour HELM

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1007 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 3e561390ef..4c68617c24 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -71,7 +71,7 @@ let (in_variable, out_variable) =
     cache_function = cache_variable;
     load_function = (fun _ -> ());
     open_function = (fun _ -> ());
-    export_function = (fun x -> None) }
+    export_function = (fun x -> Some x) }
   in
   declare_object ("VARIABLE", od)
 
-- 
cgit v1.2.3