diff options
Diffstat (limited to 'plugins/extraction/mlutil.mli')
| -rw-r--r-- | plugins/extraction/mlutil.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index b55766ed3..022e42fdd 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -11,6 +11,7 @@ open Names open Term open Libnames open Miniml +open Table (*s Utility functions over ML types with meta. *) @@ -106,7 +107,7 @@ val ast_lift : int -> ml_ast -> ml_ast val ast_pop : ml_ast -> ml_ast val ast_subst : ml_ast -> ml_ast -> ml_ast -val ast_glob_subst : ml_ast Refmap.t -> ml_ast -> ml_ast +val ast_glob_subst : ml_ast Refmap'.t -> ml_ast -> ml_ast val normalize : ml_ast -> ml_ast val optimize_fix : ml_ast -> ml_ast |