L'état implicite des définitions survivant au discharge redevient celui du moment de la définition (et non celui du moment de la fermeture de section) mais les args imps sont recalculés

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

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