From a1d00fa77939f99dd5e7ddd41c8ecf64e8af4fa1 Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Mon, 2 Dec 2019 12:52:39 +0100
Subject: Add syntax for non maximally inserted implicit arguments

---
 interp/impargs.mli | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'interp/impargs.mli')

diff --git a/interp/impargs.mli b/interp/impargs.mli
index ef3c2496f4..65e7fd8aaf 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -77,6 +77,7 @@ type implicit_side_condition
 type implicits_list = implicit_side_condition * implicit_status list
 
 val is_status_implicit : implicit_status -> bool
+val binding_kind_of_status : implicit_status -> Glob_term.binding_kind
 val is_inferable_implicit : bool -> int -> implicit_status -> bool
 val name_of_implicit : implicit_status -> Id.t
 val maximal_insertion_of : implicit_status -> bool
@@ -113,12 +114,10 @@ val declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
 val maybe_declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
   manual_implicits -> unit
 
-type implicit_kind = Implicit | MaximallyImplicit | NotImplicit
-
 (** [set_implicits local ref l]
    Manual declaration of implicit arguments.
   `l` is a list of possible sequences of implicit statuses. *)
-val set_implicits : bool -> GlobRef.t -> implicit_kind list list -> unit
+val set_implicits : bool -> GlobRef.t -> Glob_term.binding_kind list list -> unit
 
 val implicits_of_global : GlobRef.t -> implicits_list list
 
-- 
cgit v1.2.3