diff options
Diffstat (limited to 'library/impargs.mli')
| -rw-r--r-- | library/impargs.mli | 48 |
1 files changed, 43 insertions, 5 deletions
diff --git a/library/impargs.mli b/library/impargs.mli index 5b55af82..705efd31 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 10741 2008-04-02 15:47:07Z msozeau $ i*) +(*i $Id: impargs.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) (*i*) open Names @@ -20,6 +20,7 @@ open Nametab are outside the kernel, which knows nothing about implicit arguments. *) val make_implicit_args : bool -> unit +val make_manual_implicit_args : bool -> unit val make_strict_implicit_args : bool -> unit val make_strongly_strict_implicit_args : bool -> unit val make_reversible_pattern_implicit_args : bool -> unit @@ -27,6 +28,7 @@ val make_contextual_implicit_args : bool -> unit val make_maximal_implicit_args : bool -> unit val is_implicit_args : unit -> bool +val is_manual_implicit_args : unit -> bool val is_strict_implicit_args : unit -> bool val is_strongly_strict_implicit_args : unit -> bool val is_reversible_pattern_implicit_args : unit -> bool @@ -38,16 +40,25 @@ val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b (*s An [implicits_list] is a list of positions telling which arguments of a reference can be automatically infered *) -type implicit_status -type implicits_list = implicit_status list -type implicit_explanation + +type argument_position = + | Conclusion + | Hyp of int + +type implicit_explanation = + | DepRigid of argument_position + | DepFlex of argument_position + | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position + | Manual + +type implicit_status = (identifier * implicit_explanation * 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 forced_implicit : implicit_status -> bool val positions_of_implicits : implicits_list -> int list @@ -83,3 +94,30 @@ val maybe_declare_manual_implicits : bool -> global_reference -> bool -> manual_explicitation list -> unit val implicits_of_global : global_reference -> implicits_list + +val lift_implicits : int -> manual_explicitation list -> manual_explicitation list + +val merge_impls : implicits_list -> implicits_list -> implicits_list + +type implicit_interactive_request = + | ImplAuto + | ImplManual of implicit_status list + +type implicit_discharge_request = + | ImplLocal + | ImplConstant of constant * implicits_flags + | ImplMutualInductive of kernel_name * 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 + |