More comments and less doublons in some mli

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

2 files changed, 34 insertions, 9 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index 993e33b32..fad81b152 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -588,6 +588,8 @@ let declare_mib_implicits kn =
 (* Declare manual implicits *)
 type manual_explicitation = Topconstr.explicitation * (bool * bool * bool)
 
+type manual_implicits = manual_explicitation list
+
 let compute_implicits_with_manual env typ enriching l =
   let _,autoimpls = compute_auto_implicits env !implicit_args enriching typ in
   set_manual_implicits env !implicit_args enriching autoimpls l
diff --git a/library/impargs.mli b/library/impargs.mli
index a4553b0fc..631574591 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -12,9 +12,7 @@ open Term
 open Environ
 open Nametab
 
-(** Implicit Arguments *)
-
-(** {6 ... } *)
+(** {6 Implicit Arguments } *)
 (** Here we store the implicit arguments. Notice that we
     are outside the kernel, which knows nothing about implicit arguments. *)
 
@@ -44,13 +42,35 @@ type argument_position =
   | Conclusion
   | Hyp of int
 
+(** We remember various information about why an argument is
+   inferable as implicit *)
 type implicit_explanation =
   | DepRigid of argument_position
+      (** means that the implicit argument can be found by
+	  unification along a rigid path (we do not print the arguments of
+	  this kind if there is enough arguments to infer them) *)
   | DepFlex of argument_position
+      (** means that the implicit argument can be found by unification
+	  along a collapsable path only (e.g. as x in (P x) where P is another
+	  argument) (we do (defensively) print the arguments of this kind) *)
   | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position
+      (** means that the least argument from which the
+	  implicit argument can be inferred is following a collapsable path
+	  but there is a greater argument from where the implicit argument is
+	  inferable following a rigid path (useful to know how to print a
+	  partial application) *)
   | Manual
+      (** means the argument has been explicitely set as implicit. *)
+      
+(**  We also consider arguments inferable from the conclusion but it is
+     operational only if [conclusion_matters] is true. *)
 
-type implicit_status = (identifier * implicit_explanation * (bool * bool)) option
+type maximal_insertion = bool (** true = maximal contextual insertion *)
+type force_inference = bool (** true = always infer, never turn into evar/subgoal *)
+
+type implicit_status = (identifier * implicit_explanation * 
+			  (maximal_insertion * force_inference)) option
+    (** [None] = Not implicit *)
 
 type implicit_side_condition
 
@@ -67,10 +87,13 @@ val positions_of_implicits : implicits_list -> int list
 (** A [manual_explicitation] is a tuple of a positional or named explicitation with
    maximal insertion, force inference and force usage flags. Forcing usage makes
    the argument implicit even if the automatic inference considers it not inferable. *)
-type manual_explicitation = Topconstr.explicitation * (bool * bool * bool)
+type manual_explicitation = Topconstr.explicitation * 
+    (maximal_insertion * force_inference * bool)
+
+type manual_implicits = manual_explicitation list
 
 val compute_implicits_with_manual : env -> types -> bool ->
-  manual_explicitation list -> implicit_status list
+  manual_implicits -> implicit_status list
 
 (** {6 Computation of implicits (done using the global environment). } *)
 
@@ -87,19 +110,19 @@ val declare_implicits : bool -> global_reference -> unit
    Unsets implicits if [l] is empty. *)
 
 val declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
-  manual_explicitation list list -> unit
+  manual_implicits list -> unit
 
 (** If the list is empty, do nothing, otherwise declare the implicits. *)
 
 val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
-  manual_explicitation list -> unit
+  manual_implicits -> unit
 
 val implicits_of_global : global_reference -> implicits_list list
 
 val extract_impargs_data :
   implicits_list list -> ((int * int) option * implicit_status list) list
 
-val lift_implicits : int -> manual_explicitation list -> manual_explicitation list
+val lift_implicits : int -> manual_implicits -> manual_implicits
 
 val make_implicits_list : implicit_status list -> implicits_list list