2 files changed, 16 insertions, 3 deletions
diff --git a/library/impargs.ml b/library/impargs.ml
index 081bb58c1..9ffd103de 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -471,9 +471,10 @@ let rebuild_implicits (req,l) =
       | ImplAuto -> [ref,compute_global_implicits flags ref]
       | ImplManual l -> 
 	  let auto = compute_global_implicits flags ref in
+	  let auto = if flags.main then auto else List.map (fun _ -> None) auto in
 	  let l' = merge_impls auto l in [ref,l']
   in (req,l')
-
+    
 
 let (inImplicits, _) =
   declare_object {(default_object "IMPLICITS") with 
@@ -530,6 +531,10 @@ let declare_manual_implicits local ref enriching l =
   in
     add_anonymous_leaf (inImplicits (req,[ref,l']))
 
+let maybe_declare_manual_implicits local ref enriching l =
+  if l = [] then ()
+  else declare_manual_implicits local ref enriching l
+
 (*s Registration as global tables *)
 
 let init () = implicits_table := Refmap.empty
diff --git a/library/impargs.mli b/library/impargs.mli
index a9e6ccb91..e7b05f422 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -57,7 +57,7 @@ val compute_implicits : env -> types -> implicits_list
 
 (* A [manual_explicitation] is a tuple of a positional or named explicitation with
    maximal insertion and forcing flags. *)
-type manual_explicitation = Topconstr.explicitation * (bool * bool) 
+type manual_explicitation = Topconstr.explicitation * (bool * bool)
 
 val compute_implicits_with_manual : env -> types -> bool -> manual_explicitation list -> implicits_list
 
@@ -69,8 +69,16 @@ val declare_mib_implicits : mutual_inductive -> unit
 
 val declare_implicits : bool -> global_reference -> unit
 
-(* Manual declaration of which arguments are expected implicit *)
+(* [declare_manual_implicits local ref enriching l]
+   Manual declaration of which arguments are expected implicit.
+   Unsets implicits if [l] is empty. *)
+
 val declare_manual_implicits : bool -> global_reference -> bool ->
   manual_explicitation list -> unit
 
+(* If the list is empty, do nothing, otherwise declare the implicits. *)
+
+val maybe_declare_manual_implicits : bool -> global_reference -> bool ->
+  manual_explicitation list -> unit
+
 val implicits_of_global : global_reference -> implicits_list