From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- 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 daee5863..a10858e7 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