diff options
Diffstat (limited to 'kernel/mod_subst.ml')
| -rw-r--r-- | kernel/mod_subst.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 731475fb4..ed50c6d72 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -181,7 +181,7 @@ let solve_delta_kn resolve kn = let kn_of_delta resolve kn = try solve_delta_kn resolve kn - with _ -> kn + with Change_equiv_to_inline _ -> kn (** Try a 1st resolver, and then a 2nd in case it had no effect *) |