diff options
Diffstat (limited to 'tactics/dn.ml')
| -rw-r--r-- | tactics/dn.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/tactics/dn.ml b/tactics/dn.ml index 069e84fadf..e0f2016c77 100644 --- a/tactics/dn.ml +++ b/tactics/dn.ml @@ -1,6 +1,6 @@ open Util - +type 'res lookup_res = Label of 'res | Nothing | Everything module Make = functor (X : Set.OrderedType) -> @@ -42,8 +42,6 @@ struct type decompose_fun = X.t -> (Y.t * X.t list) option - type 'res lookup_res = Label of 'res | Nothing | Everything - type 'tree lookup_fun = 'tree -> (Y.t * 'tree list) lookup_res type t = Trie.t |