From 261ada6b499c1b803da3ac8ffe6bc8b3b9713709 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 7 Sep 2018 13:05:21 +0200
Subject: Remove dead code in Mod_subst.

---
 kernel/mod_subst.mli | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'kernel/mod_subst.mli')

diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 2e5211c770..8416094063 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -165,11 +165,6 @@ val replace_mp_in_kn : ModPath.t -> ModPath.t -> KerName.t -> KerName.t
    names appearing in [c] *)
 val subst_mps : substitution -> constr -> constr
 
-(** [occur_*id id sub] returns true iff [id] occurs in [sub]
-   on either side *)
-
-val occur_mbid : MBId.t -> substitution -> bool
-
 (** [repr_substituted r] dumps the representation of a substituted:
     - [None, a] when r is a value
     - [Some s, a] when r is a delayed substitution [s] applied to [a] *)
-- 
cgit v1.2.3