In manual implicit arguments mode, do not enrich implicits

by the automatically infered arguments.


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

2 files changed, 9 insertions, 5 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index bb11ce2f8d..b477d94958 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -71,6 +71,7 @@ let make_maximal_implicit_args flag =
 
 let is_implicit_args () = !implicit_args.main
 let is_manual_implicit_args () = !implicit_args.manual
+let is_auto_implicit_args () = !implicit_args.main && not (is_manual_implicit_args ())
 let is_strict_implicit_args () = !implicit_args.strict
 let is_strongly_strict_implicit_args () = !implicit_args.strongly_strict
 let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern
@@ -577,10 +578,11 @@ type manual_explicitation = Topconstr.explicitation * (bool * bool)
 let compute_implicits_with_manual env typ enriching l = 
   compute_manual_implicits env !implicit_args typ enriching l
 
-let declare_manual_implicits local ref enriching l =
+let declare_manual_implicits local ref ?enriching l =
   let flags = !implicit_args in
   let env = Global.env () in
   let t = Global.type_of_global ref in
+  let enriching = Option.default (is_auto_implicit_args ()) enriching in
   let l' = compute_manual_implicits env flags t enriching l in
   let req =
     if local or isVarRef ref then ImplLocal
@@ -588,9 +590,9 @@ 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 =
+let maybe_declare_manual_implicits local ref ?enriching l =
   if l = [] then ()
-  else declare_manual_implicits local ref enriching l
+  else declare_manual_implicits local ref ?enriching l
 
 let lift_implicits n = 
   List.map (fun x -> 
diff --git a/library/impargs.mli b/library/impargs.mli
index 353f657c6a..0eba9f3802 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -83,14 +83,16 @@ val declare_implicits : bool -> global_reference -> unit
 
 (* [declare_manual_implicits local ref enriching l]
    Manual declaration of which arguments are expected implicit.
+   If not set, we decide if it should enrich by automatically inferd
+   implicits depending on the current state.
    Unsets implicits if [l] is empty. *)
 
-val declare_manual_implicits : bool -> global_reference -> bool ->
+val declare_manual_implicits : bool -> global_reference -> ?enriching: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 ->
+val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
   manual_explicitation list -> unit
 
 val implicits_of_global : global_reference -> implicits_list