diff options
Diffstat (limited to 'kernel/pre_env.ml')
-rw-r--r-- | kernel/pre_env.ml | 2 |
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 |