diff options
Diffstat (limited to 'pretyping/term_dnet.mli')
| -rw-r--r-- | pretyping/term_dnet.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/term_dnet.mli b/pretyping/term_dnet.mli index ccf962481..f6c1b5b61 100644 --- a/pretyping/term_dnet.mli +++ b/pretyping/term_dnet.mli @@ -102,6 +102,8 @@ sig (* [find_all dn] returns all idents contained in dn *) val find_all : t -> ident list + + val map : (ident -> ident) -> t -> t end module Make : |