out_variable (Liboject.obj -> ...) distibgue de get_variable

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

3 files changed, 9 insertions, 6 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 2383ca304f..7a15b48637 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -69,7 +69,7 @@ let open_variable _ = ()
 
 let specification_variable x = x
 
-let (in_variable, _ (* out_variable *) ) =
+let (in_variable, out_variable) =
   let od = {
     cache_function = cache_variable;
     load_function = load_variable;
@@ -77,6 +77,8 @@ let (in_variable, _ (* out_variable *) ) =
     specification_function = specification_variable } in
   declare_object ("VARIABLE", od)
 
+let out_variable sp = fst (out_variable sp)
+
 let declare_variable id obj =
   let _ = add_leaf id CCI (in_variable ((id,obj),is_implicit_args())) in
   ()
@@ -207,7 +209,7 @@ let constant_or_parameter_strength sp =
 let is_variable id = 
   let sp = Nametab.sp_of_id CCI id in Spmap.mem sp !vartab
   
-let out_variable sp = 
+let get_variable sp = 
   let (id,(_,str,sticky)) = Spmap.find sp !vartab in
   let (c,ty) = Global.lookup_named id in
   ((id,c,ty),str,sticky)
diff --git a/library/declare.mli b/library/declare.mli
index 6dfcb40650..db27ccf986 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -56,7 +56,8 @@ val constant_strength : section_path -> strength
 val constant_or_parameter_strength : section_path -> strength
 
 val is_variable : identifier -> bool
-val out_variable : section_path -> named_declaration * strength * sticky
+val out_variable : Libobject.obj -> identifier * variable_declaration
+val get_variable : section_path -> named_declaration * strength * sticky
 val variable_strength : identifier -> strength
 
 
@@ -64,7 +65,8 @@ val variable_strength : identifier -> strength
     construtor) corresponding to [id] in global environment, together
     with its definition environment. *)
 
-val global_operator : path_kind -> identifier -> global_reference * named_context
+val global_operator : 
+  path_kind -> identifier -> global_reference * named_context
 
 (*s [global_reference k id] returns the object corresponding to
     the name [id] in the global environment. It may be a constant, 
diff --git a/library/library.ml b/library/library.ml
index d938bd635c..4a76bff1c1 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -12,8 +12,7 @@ open Lib
 
 let loadpath_name = "LoadPath"
 
-module LoadPath =
-struct
+module LoadPath = struct
   let check s = if not (System.exists_dir s) then warning (s^" was not found")
   let key = Goptions.PrimaryTable loadpath_name
   let title = "Load Paths for Coq files"