diff options
Diffstat (limited to 'contrib/extraction/modutil.mli')
-rw-r--r-- | contrib/extraction/modutil.mli | 16 |
1 files changed, 3 insertions, 13 deletions
diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli index 85d58a4b..e279261d 100644 --- a/contrib/extraction/modutil.mli +++ b/contrib/extraction/modutil.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modutil.mli 10620 2008-03-05 10:54:41Z letouzey $ i*) +(*i $Id: modutil.mli 11602 2008-11-18 00:08:33Z letouzey $ i*) open Names open Declarations @@ -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 @@ -30,15 +24,11 @@ type do_ref = global_reference -> unit val decl_iter_references : do_ref -> do_ref -> do_ref -> ml_decl -> unit val spec_iter_references : do_ref -> do_ref -> do_ref -> ml_spec -> unit -val struct_iter_references : do_ref -> do_ref -> do_ref -> ml_structure -> unit - -type 'a kinds = { mutable typ : 'a ; mutable trm : 'a; mutable cons : 'a } - -val struct_get_references_set : ml_structure -> Refset.t kinds -val struct_get_references_list : ml_structure -> global_reference list kinds val signature_of_structure : ml_structure -> ml_signature +val msid_of_mt : ml_module_type -> module_path + val get_decl_in_structure : global_reference -> ml_structure -> ml_decl (* Some transformations of ML terms. [optimize_struct] simplify |