summaryrefslogtreecommitdiff
path: root/library/impargs.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/impargs.mli')
-rw-r--r--library/impargs.mli29
1 files changed, 10 insertions, 19 deletions
diff --git a/library/impargs.mli b/library/impargs.mli
index c1f119e6..e8191e86 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: impargs.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
+(*i $Id$ i*)
(*i*)
open Names
@@ -16,7 +16,7 @@ open Environ
open Nametab
(*i*)
-(*s Implicit arguments. Here we store the implicit arguments. Notice that we
+(*s Implicit arguments. Here we store the implicit arguments. Notice that we
are outside the kernel, which knows nothing about implicit arguments. *)
val make_implicit_args : bool -> unit
@@ -50,13 +50,14 @@ type implicit_explanation =
| DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position
| Manual
-type implicit_status = (identifier * implicit_explanation * bool) option
+type implicit_status = (identifier * implicit_explanation * (bool * bool)) option
type implicits_list = implicit_status list
val is_status_implicit : implicit_status -> bool
val is_inferable_implicit : bool -> int -> implicit_status -> bool
val name_of_implicit : implicit_status -> identifier
val maximal_insertion_of : implicit_status -> bool
+val force_inference_of : implicit_status -> bool
val positions_of_implicits : implicits_list -> int list
@@ -65,10 +66,11 @@ val positions_of_implicits : implicits_list -> int list
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)
+ 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)
-val compute_implicits_with_manual : env -> types -> bool ->
+val compute_implicits_with_manual : env -> types -> bool ->
manual_explicitation list -> implicits_list
(*s Computation of implicits (done using the global environment). *)
@@ -106,18 +108,7 @@ type implicit_interactive_request =
type implicit_discharge_request =
| ImplLocal
| ImplConstant of constant * implicits_flags
- | ImplMutualInductive of kernel_name * implicits_flags
- | ImplInteractive of global_reference * implicits_flags *
+ | ImplMutualInductive of mutual_inductive * implicits_flags
+ | ImplInteractive of global_reference * implicits_flags *
implicit_interactive_request
-val discharge_implicits : 'a *
- (implicit_discharge_request *
- (Libnames.global_reference *
- (Names.identifier * implicit_explanation * bool) option list)
- list) ->
- (implicit_discharge_request *
- (Libnames.global_reference *
- (Names.identifier * implicit_explanation * bool) option list)
- list)
- option
-