2 files changed, 23 insertions, 0 deletions
diff --git a/library/impargs.ml b/library/impargs.ml
index 61a2c8b1a0..a8fe59cc80 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -23,6 +23,11 @@ let auto_implicits ty =
   else
     No_impl
 
+let list_of_implicits = function 
+  | Impl_auto l -> l
+  | Impl_manual l -> l
+  | No_impl -> []
+
 (* Constants. *)
 
 let constants_table = ref Spmap.empty
@@ -63,6 +68,17 @@ let constructor_implicits ((sp,i),j) =
   let imps = Spmap.find sp !inductives_table in
   (snd imps.(i)).(pred j)
 
+let mconstr_implicits mc = 
+  let (sp, i, j, _) = destMutConstruct mc in
+  list_of_implicits (constructor_implicits ((sp,i),j))
+
+let mind_implicits m =
+  let (sp,i,_) = destMutInd m in
+  list_of_implicits (inductive_implicits (sp,i))
+
+let implicits_of_var kind id =
+  failwith "TODO: implicits of vars"
+
 (* Registration as global tables and roolback. *)
 
 type frozen = implicits Spmap.t
@@ -85,3 +101,4 @@ let _ =
 let rollback f x =
   let fs = freeze () in
   try f x with e -> begin unfreeze fs; raise e end
+
diff --git a/library/impargs.mli b/library/impargs.mli
index 84ea98da35..51ada5845a 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -3,6 +3,7 @@
 
 (*i*)
 open Names
+open Term
 (*i*)
 
 (* Implicit arguments. Here we store the implicit arguments. Notice that we 
@@ -15,6 +16,8 @@ type implicits =
 
 val implicit_args : bool ref
 
+val list_of_implicits : implicits -> int list
+
 val declare_constant_implicits : section_path -> unit
 val declare_constant_manual_implicits : section_path -> int list -> unit
 val constant_implicits : section_path -> implicits
@@ -23,4 +26,7 @@ val declare_inductive_implicits : section_path -> unit
 val inductive_implicits : section_path * int -> implicits
 val constructor_implicits : (section_path * int) * int -> implicits
 
+val mconstr_implicits : constr -> int list
+val mind_implicits : constr -> int list
+val implicits_of_var : Names.path_kind -> identifier -> int list