Implicit arguments in class field declarations

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

2 files changed, 13 insertions, 9 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index 4272f413a..687374c59 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -257,9 +257,7 @@ let rec assoc_by_pos k = function
   | hd :: tl -> let (x, tl) = assoc_by_pos k tl in x, hd :: tl
   | [] -> raise Not_found
 
-let compute_manual_implicits flags ref enriching l =
-  let t = Global.type_of_global ref in
-  let env = Global.env () in
+let compute_manual_implicits flags env t enriching l =
   let autoimps =
     if enriching then compute_implicits_flags env flags true t
     else compute_implicits_gen false false false true true env t in
@@ -517,9 +515,14 @@ let declare_mib_implicits kn =
 (* Declare manual implicits *)
 type manual_explicitation = Topconstr.explicitation * (bool * bool) 
 
+let compute_implicits_with_manual env typ enriching l = 
+  compute_manual_implicits !implicit_args env typ enriching l
+
 let declare_manual_implicits local ref enriching l =
   let flags = !implicit_args in
-  let l' = compute_manual_implicits flags ref enriching l in
+  let env = Global.env () in
+  let t = Global.type_of_global ref in
+  let l' = compute_manual_implicits flags env t enriching l in
   let req =
     if local or isVarRef ref then ImplNoDischarge
     else ImplInteractive(ref,flags,ImplManual l')
diff --git a/library/impargs.mli b/library/impargs.mli
index 22c1ea23c..a9e6ccb91 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -55,6 +55,12 @@ val positions_of_implicits : implicits_list -> int list
    for an object of the given type in the given env *)
 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) 
+
+val compute_implicits_with_manual : env -> types -> bool -> manual_explicitation list -> implicits_list
+
 (*s Computation of implicits (done using the global environment). *)
 
 val declare_var_implicits : variable -> unit
@@ -63,13 +69,8 @@ val declare_mib_implicits : mutual_inductive -> unit
 
 val declare_implicits : bool -> global_reference -> unit
 
-(* 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) 
-
 (* Manual declaration of which arguments are expected implicit *)
 val declare_manual_implicits : bool -> global_reference -> bool ->
   manual_explicitation list -> unit
 
 val implicits_of_global : global_reference -> implicits_list
-