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

5 files changed, 13 insertions, 10 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"
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 288581c674..7300f126bc 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -186,7 +186,7 @@ let print_mutual sp mib =
              implicit_args_msg sp mipv >])
 
 let print_section_variable sp =
-  let ((id,_,_) as d,_,_) = out_variable sp in
+  let ((id,_,_) as d,_,_) = get_variable sp in
   let l = implicits_of_var id in
   [< print_named_decl d; print_impl_args l; 'fNL >]
 
@@ -329,7 +329,7 @@ let crible (fn : string -> env -> constr -> unit) name =
     | (spopt,Lib.Leaf lobj)::rest ->
 	(match (spopt,object_tag lobj) with
 	   | (_,"VARIABLE") ->
-	       let ((idc,_,typ),_,_) = out_variable spopt in 
+	       let ((idc,_,typ),_,_) = get_variable spopt in 
                if (head_const (body_of_type typ)) = const then  
                  fn (string_of_id idc) env (body_of_type typ);
                crible_rec rest
@@ -454,7 +454,7 @@ let print_local_context () =
     | [] -> [< >]
     | (sp,Lib.Leaf lobj)::rest ->
 	if "VARIABLE" = object_tag lobj then
-          let (d,_,_) = out_variable sp in 
+          let (d,_,_) = get_variable sp in 
 	  [< print_var_rec rest;
              print_named_decl d >]
 	else 
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 5b09315d98..01e58b3441 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -131,7 +131,7 @@ let process_object oldenv sec_sp (ops,ids_to_discard,work_alist) (sp,lobj) =
   let tag = object_tag lobj in 
   match tag with
     | "VARIABLE" ->
-	let ((id,c,t),stre,sticky) = out_variable sp in
+	let ((id,c,t),stre,sticky) = get_variable sp in
 	if stre = (DischargeAt sec_sp) or ids_to_discard <> [] then
 	  (ops,id::ids_to_discard,work_alist)
 	else