From f50bbdc50b21083f65f0e415e7f2edff6f11e45f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 18 Sep 2020 10:11:24 +0200 Subject: Remove unused API from Dn. --- tactics/dn.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'tactics/dn.mli') diff --git a/tactics/dn.mli b/tactics/dn.mli index 287aa2b257..85f9ef6dfb 100644 --- a/tactics/dn.mli +++ b/tactics/dn.mli @@ -38,6 +38,4 @@ sig val lookup : t -> 'term lookup_fun -> 'term -> Z.t list - val app : (Z.t -> unit) -> t -> unit - end -- cgit v1.2.3