diff options
Diffstat (limited to 'contrib/extraction/common.mli')
| -rw-r--r-- | contrib/extraction/common.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli index 7dae2ae19..2d3a7d47b 100644 --- a/contrib/extraction/common.mli +++ b/contrib/extraction/common.mli @@ -10,10 +10,16 @@ open Pp open Names +open Declarations +open Environ open Libnames open Miniml open Mlutil +val add_structure : module_path -> module_structure_body -> env -> env + +val add_functor : mod_bound_id -> module_type_body -> env -> env + val print_one_decl : ml_structure -> module_path -> ml_decl -> unit |