2 files changed, 24 insertions, 2 deletions
diff --git a/library/impargs.ml b/library/impargs.ml
index 17cd54b2c6..8dc830fae0 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -19,10 +19,10 @@ let implicit_args = ref false
 let make_implicit_args flag = implicit_args := flag
 let is_implicit_args () = !implicit_args
 
-let implicitely f x =
+let with_implicits b f x =
   let oimplicit = !implicit_args in
   try 
-    implicit_args := true;
+    implicit_args := b;
     let rslt = f x in 
     implicit_args := oimplicit;
     rslt
@@ -31,6 +31,12 @@ let implicitely f x =
     raise e
   end
 
+let implicitely f = with_implicits true f
+
+let using_implicits = function
+  | No_impl -> with_implicits false
+  | _ -> with_implicits true
+
 let auto_implicits env ty = Impl_auto (poly_args env Evd.empty ty)
 
 let list_of_implicits = function 
@@ -107,6 +113,17 @@ let declare_var_implicits id =
 let implicits_of_var id =
   list_of_implicits (try Idmap.find id !var_table with Not_found -> No_impl)
 
+(* Tests if declared implicit *)
+
+let is_implicit_constant sp =
+  try let _ = Spmap.find sp !constants_table in true with Not_found -> false
+
+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
+
 (* Registration as global tables and roolback. *)
 
 type frozen_t = bool
diff --git a/library/impargs.mli b/library/impargs.mli
index 8af10d7ec9..828cc4050d 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -18,6 +18,7 @@ type implicits =
 val make_implicit_args : bool -> unit
 val is_implicit_args : unit -> bool
 val implicitely : ('a -> 'b) -> 'a -> 'b
+val with_implicits : bool -> ('a -> 'b) -> 'a -> 'b
 
 val list_of_implicits : implicits -> int list
 
@@ -36,6 +37,10 @@ val constant_implicits_list : section_path -> int list
 val declare_var_implicits : identifier -> unit
 val implicits_of_var : identifier -> int list
 
+val is_implicit_constant : section_path -> bool
+val is_implicit_inductive_definition : section_path -> bool
+val is_implicit_var : identifier -> bool
+
 type frozen_t
 val freeze : unit -> frozen_t
 val unfreeze : frozen_t -> unit