diff options
Diffstat (limited to 'contrib/extraction/modutil.mli')
| -rw-r--r-- | contrib/extraction/modutil.mli | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli index ee5ea709f..670a5a6c2 100644 --- a/contrib/extraction/modutil.mli +++ b/contrib/extraction/modutil.mli @@ -15,12 +15,6 @@ open Libnames open Miniml open Mod_subst -(*s Functions upon modules missing in [Modops]. *) - -(* Change a msid in a module type, to follow a module expr. *) - -val replicate_msid : struct_expr_body -> struct_expr_body -> struct_expr_body - (*s Functions upon ML modules. *) val struct_ast_search : (ml_ast -> bool) -> ml_structure -> bool |