diff options
Diffstat (limited to 'checker/declarations.ml')
| -rw-r--r-- | checker/declarations.ml | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index 0e5eb0c23..70f16158e 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -135,16 +135,6 @@ let delta_of_mp resolve mp = | _ -> anomaly "mod_subst: bad association in delta_resolver" with Not_found -> mp - -let delta_of_kn resolve kn = - try - match Deltamap.find (KN kn) resolve with - | Equiv kn1 -> kn1 - | Inline _ -> kn - | _ -> anomaly - "mod_subst: bad association in delta_resolver" - with - Not_found -> kn let remove_mp_delta_resolver resolver mp = Deltamap.remove (MP mp) resolver |