From 693d398b5e4e55a916bbdaa8e4c23c83d9dbcef7 Mon Sep 17 00:00:00 2001 From: notin Date: Wed, 25 Jun 2008 18:19:21 +0000 Subject: Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisation (add_glob* et dump_*) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11177 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/modintern.mli | 3 --- 1 file changed, 3 deletions(-) (limited to 'interp/modintern.mli') diff --git a/interp/modintern.mli b/interp/modintern.mli index c14b6481e..1f27e3c18 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -26,6 +26,3 @@ val interp_modtype : env -> module_type_ast -> module_struct_entry val interp_modexpr : env -> module_ast -> module_struct_entry val lookup_module : qualid located -> module_path - -val dump_moddef : loc -> module_path -> string -> unit -val dump_modref : loc -> module_path -> string -> unit -- cgit v1.2.3