diff options
Diffstat (limited to 'tactics/term_dnet.mli')
| -rw-r--r-- | tactics/term_dnet.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/term_dnet.mli b/tactics/term_dnet.mli index a5c80cc0..58f95ac6 100644 --- a/tactics/term_dnet.mli +++ b/tactics/term_dnet.mli @@ -80,6 +80,8 @@ sig val find_all : t -> ident list val map : (ident -> ident) -> t -> t + + val refresh_metas : t -> t end module Make : |