diff options
Diffstat (limited to 'contrib/extraction/mlutil.mli')
| -rw-r--r-- | contrib/extraction/mlutil.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli index abec7a65d..1b8166b58 100644 --- a/contrib/extraction/mlutil.mli +++ b/contrib/extraction/mlutil.mli @@ -41,6 +41,8 @@ val clear_singletons : unit -> unit n] occurs (freely) in [t]. [ml_lift] is de Bruijn lifting. [ml_subst e t] substitutes [e] for [Rel 1] in [t]. *) +val ast_iter : (ml_ast -> unit) -> ml_ast -> unit + val occurs : int -> ml_ast -> bool val ml_lift : int -> ml_ast -> ml_ast |