diff options
author | 2016-08-19 20:34:40 +0200 | |
---|---|---|
committer | 2016-08-19 20:34:59 +0200 | |
commit | 82dc377451e2dc7810eea136b9a6ab8fc5ae48b5 (patch) | |
tree | 19336aad14e3e1c40dd8ee88f058d8d518e1c42f /library/impargs.mli | |
parent | 05f3192fedc354eb34ac10813bd7f1ffadfd4405 (diff) |
Removing dead code in Impargs.
Diffstat (limited to 'library/impargs.mli')
-rw-r--r-- | library/impargs.mli | 12 |
1 files changed, 1 insertions, 11 deletions
diff --git a/library/impargs.mli b/library/impargs.mli index 34e529ca2..327f84d9f 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -29,8 +29,7 @@ val is_reversible_pattern_implicit_args : unit -> bool val is_contextual_implicit_args : unit -> bool val is_maximal_implicit_args : unit -> bool -type implicits_flags -val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b +val with_implicits : ('a -> 'b) -> 'a -> 'b (** {6 ... } *) (** An [implicits_list] is a list of positions telling which arguments @@ -136,14 +135,5 @@ val select_impargs_size : int -> implicits_list list -> implicit_status list val select_stronger_impargs : implicits_list list -> implicit_status list -type implicit_interactive_request - -type implicit_discharge_request = - | ImplLocal - | ImplConstant of constant * implicits_flags - | ImplMutualInductive of mutual_inductive * implicits_flags - | ImplInteractive of global_reference * implicits_flags * - implicit_interactive_request - val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool (** Equality on [explicitation]. *) |