From 1d651163f5a0d5cc9c06059e29332c493ec70664 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 11 Oct 2011 19:18:46 +0000 Subject: Mod_subst: an unused function git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14551 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/mod_subst.mli | 4 ---- 1 file changed, 4 deletions(-) (limited to 'kernel/mod_subst.mli') diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index e06cc816d..90b3d8c69 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -55,10 +55,6 @@ val delta_of_mp : delta_resolver -> module_path -> module_path (** Extract the set of inlined constant in the resolver *) val inline_of_delta : int option -> delta_resolver -> (int * kernel_name) list -(** remove_mp is used for the computation of a resolver induced by Include P *) -val remove_mp_delta_resolver : delta_resolver -> module_path -> delta_resolver - - (** mem tests *) val mp_in_delta : module_path -> delta_resolver -> bool -- cgit v1.2.3