From 4cddb7d0765a091c6514a85475dcdd7af34aaf29 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 1 Mar 2014 16:34:54 +0100 Subject: Never suppress the typing constraint of bound variables whose name was reserved with Implicit Type. --- interp/reserve.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'interp/reserve.mli') diff --git a/interp/reserve.mli b/interp/reserve.mli index de72a410d..8ae55d096 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -14,4 +14,3 @@ open Notation_term val declare_reserved_type : Id.t located list -> notation_constr -> unit val find_reserved_type : Id.t -> notation_constr -val anonymize_if_reserved : Name.t -> glob_constr -> glob_constr -- cgit v1.2.3