diff options
| -rw-r--r-- | kernel/mod_subst.ml | 15 | ||||
| -rw-r--r-- | kernel/mod_subst.mli | 5 |
2 files changed, 0 insertions, 20 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index b35b9dda31..8a4c359470 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -61,7 +61,6 @@ module Umap = struct let add_mp mp x (m1,m2) = (MPmap.add mp x m1, m2) let find_mp mp map = MPmap.find mp (fst map) let find_mbi mbi map = MBImap.find mbi (snd map) - let iter_mbi f map = MBImap.iter f (snd map) let fold fmp fmbi (m1,m2) i = MPmap.fold fmp m1 (MBImap.fold fmbi m2 i) let join map1 map2 = fold add_mp add_mbi map1 map2 @@ -551,20 +550,6 @@ let join subst1 subst2 = let subst = Umap.fold mp_apply_subst mbi_apply_subst subst1 empty_subst in Umap.join subst2 subst -let rec occur_in_path mbi = function - | MPbound bid' -> MBId.equal mbi bid' - | MPdot (mp1,_) -> occur_in_path mbi mp1 - | _ -> false - -let occur_mbid mbi sub = - let check_one mbi' (mp,_) = - if MBId.equal mbi mbi' || occur_in_path mbi mp then raise Exit - in - try - Umap.iter_mbi check_one sub; - false - with Exit -> true - type 'a substituted = { mutable subst_value : 'a; mutable subst_subst : substitution list; 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] *) |