aboutsummaryrefslogtreecommitdiff
path: root/kernel/pre_env.ml
diff options
context:
space:
mode:
authorletouzey2013-03-13 00:00:17 +0000
committerletouzey2013-03-13 00:00:17 +0000
commit9aecb4427f0f8ca3cb4c26bc7f73bb74164a93d9 (patch)
tree36a4ab30f4a75e73c9f4921cca1d25d1cb7cd545 /kernel/pre_env.ml
parent552df1605233769ad3cdabaadaa0011605e79797 (diff)
Restrict (try...with...) to avoid catching critical exn (part 8)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/pre_env.ml')
-rw-r--r--kernel/pre_env.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 2a467ad0a9..f365d19c3f 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -90,7 +90,7 @@ let push_rel d env =
let lookup_rel_val n env =
try List.nth env.env_rel_val (n - 1)
- with _ -> raise Not_found
+ with Failure _ -> raise Not_found
let env_of_rel n env =
{ env with