ajouts divers pour module Printer

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

4 files changed, 13 insertions, 3 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 6336c03c6f..aca22ebd2c 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -161,14 +161,14 @@ let mind_oper_of_id sp id mib =
 
 let global_operator sp id =
   try
-    let _ = Global.lookup_constant sp in Const sp
+    let cb = Global.lookup_constant sp in Const sp, cb.const_hyps
   with Not_found -> 
     let mib = Global.lookup_mind sp in
-    mind_oper_of_id sp id mib
+    mind_oper_of_id sp id mib, mib.mind_hyps
 
 let global_reference kind id =
   let sp = Nametab.sp_of_id kind id in
-  let oper = global_operator sp id in
+  let (oper,_) = global_operator sp id in
   let hyps = get_globals (Global.context ()) in
   let ids = ids_of_sign hyps in
   DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids))
diff --git a/library/declare.mli b/library/declare.mli
index e833d0bb80..9b0f969820 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -4,6 +4,7 @@
 (*i*)
 open Names
 open Term
+open Sign
 open Constant
 open Inductive
 (*i*)
@@ -36,6 +37,7 @@ val declare_eliminations : section_path -> unit
   then constructs the corresponding term, associated to the current 
   environment of variables. *)
 
+val global_operator : section_path -> identifier -> sorts oper * var_context
 val global_reference : path_kind -> identifier -> constr
 
 val is_global : identifier -> bool
diff --git a/library/global.ml b/library/global.ml
index e6c4008067..3525d38344 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -45,6 +45,10 @@ let lookup_mind_specif c = lookup_mind_specif c !global_env
 let export s = export !global_env s
 let import cenv = global_env := import cenv !global_env
 
+(* Some instanciations of functions from [Environ]. *)
+
+let id_of_global = id_of_global !global_env
+
 (* Re-exported functions of [Inductive], composed with [lookup_mind_specif]. *)
 
 open Inductive
diff --git a/library/global.mli b/library/global.mli
index 4e186d35b5..22623424bb 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -38,6 +38,10 @@ val lookup_mind_specif : constr -> mind_specif
 val export : string -> compiled_env
 val import : compiled_env -> unit
 
+(*s Some functions of [Environ] instanciated on the global environment. *)
+
+val id_of_global : sorts oper -> identifier
+
 (*s Re-exported functions of [Inductive], composed with 
     [lookup_mind_specif]. *)