diff options
Diffstat (limited to 'tactics/dn.mli')
| -rw-r--r-- | tactics/dn.mli | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/tactics/dn.mli b/tactics/dn.mli index 2a60c3eb82..287aa2b257 100644 --- a/tactics/dn.mli +++ b/tactics/dn.mli @@ -18,9 +18,13 @@ sig must decompose any tree into a label characterizing its root node and the list of its subtree *) - val add : t -> 'a decompose_fun -> 'a * Z.t -> t + type pattern - val rmv : t -> 'a decompose_fun -> 'a * Z.t -> t + val pattern : 'a decompose_fun -> 'a -> pattern + + val add : t -> pattern -> Z.t -> t + + val rmv : t -> pattern -> Z.t -> t type 'tree lookup_fun = 'tree -> (Y.t * 'tree list) lookup_res |