diff options
| author | Pierre-Marie Pédrot | 2014-03-03 02:22:56 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-03-03 02:34:17 +0100 |
| commit | 37f624d80e82d655021f2beb7d72794a120ff8b5 (patch) | |
| tree | 35954a2abc642ebc3f8a2cec54082bf43dcde7f7 /tactics/dn.ml | |
| parent | b076e7f88124db576c4f3c06e2ac93673236be7a (diff) | |
Extruding code not depending of the functor argument in Termdn.
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 |