diff options
Diffstat (limited to 'kernel/mod_subst.ml')
| -rw-r--r-- | kernel/mod_subst.ml | 15 |
1 files changed, 0 insertions, 15 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; |