summaryrefslogtreecommitdiff
path: root/kernel/pre_env.ml
diff options
context:
space:
mode:
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 6c08c34c..f0a3292c 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 e when Errors.noncritical e -> raise Not_found
let env_of_rel n env =
{ env with