diff options
| author | Hugo Herbelin | 2020-09-19 18:02:42 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-19 18:02:42 +0200 |
| commit | fff4fe1120c81ab7b543cfb8d175cc4458e3c12e (patch) | |
| tree | f6600997d01306f371526b905e5dfaf26c0f4afd /tactics/dn.mli | |
| parent | 9809e48867867b26844656a1368dcb88a83c36ed (diff) | |
| parent | f50bbdc50b21083f65f0e415e7f2edff6f11e45f (diff) | |
Merge PR #13052: Clean up Dnet implementation
Reviewed-by: herbelin
Diffstat (limited to 'tactics/dn.mli')
| -rw-r--r-- | tactics/dn.mli | 2 |
1 files changed, 0 insertions, 2 deletions
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 |