From 0ade32f84b28d2190360ec79520788142755b5b7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 11 Mar 2018 20:29:16 +0100 Subject: [api] Deprecate a couple of aliases that we missed. --- interp/impargs.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/impargs.mli') diff --git a/interp/impargs.mli b/interp/impargs.mli index 1eeb8e41a..103a4f9e9 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -130,7 +130,7 @@ val make_implicits_list : implicit_status list -> implicits_list list val drop_first_implicits : int -> implicits_list -> implicits_list -val projection_implicits : env -> projection -> implicit_status list -> +val projection_implicits : env -> Projection.t -> implicit_status list -> implicit_status list val select_impargs_size : int -> implicits_list list -> implicit_status list -- cgit v1.2.3