diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-12 23:59:39 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-12 23:59:39 +0000 |
| commit | 701381d9280fa6948a4ab8ab4ad36c8674bad903 (patch) | |
| tree | 9e4dd83d6dbc7aafa7e556a522ad8e9058012f8d /kernel/mod_subst.ml | |
| parent | 8aa2e600d375caffef47058f1d095777a0dfdbb0 (diff) | |
Restrict (try...with...) to avoid catching critical exn (part 2)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16277 85f007b7-540e-0410-9357-904b9bb8a0f7
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 *) |