Ajout implicits_of_global + accès par noms longs

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

2 files changed, 23 insertions, 14 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index c9fa33e24d..5248bc4a61 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -101,16 +101,16 @@ let inductive_implicits_list ind_sp =
 
 (* Variables. *)
 
-let var_table = ref Idmap.empty
+let var_table = ref Spmap.empty
 
-let declare_var_implicits id =
+let declare_var_implicits sp =
   let env = Global.env () in
-  let (_,ty) = lookup_named id env in
+  let (_,ty) = lookup_named (basename sp) env in
   let imps = auto_implicits env (body_of_type ty) in
-  var_table := Idmap.add id imps !var_table
+  var_table := Spmap.add sp imps !var_table
 
-let implicits_of_var id =
-  list_of_implicits (try Idmap.find id !var_table with Not_found -> No_impl)
+let implicits_of_var sp =
+  list_of_implicits (try Spmap.find sp !var_table with Not_found -> No_impl)
 
 (* Tests if declared implicit *)
 
@@ -120,20 +120,27 @@ let is_implicit_constant sp =
 let is_implicit_inductive_definition sp =
   try let _ = Spmap.find sp !inductives_table in true with Not_found -> false
 
-let is_implicit_var id =
-  try let _ = Idmap.find id !var_table in true with Not_found -> false
+let is_implicit_var sp =
+  try let _ = Spmap.find sp !var_table in true with Not_found -> false
 
-(* Registration as global tables and rollback. *)
+let implicits_of_global = function
+  | VarRef sp -> implicits_of_var sp
+  | ConstRef sp -> list_of_implicits (constant_implicits sp)
+  | IndRef isp -> list_of_implicits (inductive_implicits isp)
+  | ConstructRef csp ->	list_of_implicits (constructor_implicits csp)
+  | EvarRef _ -> []
+
+(* Registration as global tables and roolback. *)
 
 type frozen_t = bool
               * implicits Spmap.t 
               * (implicits * implicits array) array Spmap.t 
-              * implicits Idmap.t
+              * implicits Spmap.t
 
 let init () =
   constants_table := Spmap.empty;
   inductives_table := Spmap.empty;
-  var_table := Idmap.empty
+  var_table := Spmap.empty
 
 let freeze () =
   (!implicit_args, !constants_table, !inductives_table, !var_table)
diff --git a/library/impargs.mli b/library/impargs.mli
index 828cc4050d..cbe31a3af2 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -34,12 +34,14 @@ val constructor_implicits_list : constructor_path -> int list
 val inductive_implicits_list : inductive_path -> int list
 val constant_implicits_list : section_path -> int list
 
-val declare_var_implicits : identifier -> unit
-val implicits_of_var : identifier -> int list
+val declare_var_implicits : section_path -> unit
+val implicits_of_var : section_path -> int list
 
 val is_implicit_constant : section_path -> bool
 val is_implicit_inductive_definition : section_path -> bool
-val is_implicit_var : identifier -> bool
+val is_implicit_var : section_path -> bool
+
+val implicits_of_global : global_reference -> int list
 
 type frozen_t
 val freeze : unit -> frozen_t