diff options
| -rw-r--r-- | checker/declarations.ml | 6 | ||||
| -rw-r--r-- | kernel/mod_subst.ml | 2 |
2 files changed, 3 insertions, 5 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index 503460422..69dd26130 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -139,10 +139,8 @@ let solve_delta_kn resolve kn = make_kn new_mp dir l let gen_of_delta resolve x kn fix_can = - try - let new_kn = solve_delta_kn resolve kn in - if kn == new_kn then x else fix_can new_kn - with _ -> x + let new_kn = solve_delta_kn resolve kn in + if kn == new_kn then x else fix_can new_kn let constant_of_delta resolve con = let kn = user_con con in 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 *) |