From 58630ad9a0b94a804a39a3d99f982965292692c7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 21 May 2018 23:54:55 +0200 Subject: [api] Misctypes removal: miscellaneous aliases. --- interp/reserve.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/reserve.mli') diff --git a/interp/reserve.mli b/interp/reserve.mli index daee58639..a10858e71 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -11,5 +11,5 @@ open Names open Notation_term -val declare_reserved_type : Misctypes.lident list -> notation_constr -> unit +val declare_reserved_type : lident list -> notation_constr -> unit val find_reserved_type : Id.t -> notation_constr -- cgit v1.2.3