aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-04-04 10:41:18 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-04-04 10:41:18 +0200
commitca0d97dd3b3033e7f87dd5e5ea09ab6f14fd881b (patch)
tree7c5d8307a7617567fb347033d9a075b69ddc529a /kernel
parent32bf31fda75918bf2910301dffa7b3137c81b236 (diff)
Fix bug #5435: [Eval native_compute in] raises anomaly.
Was introduced by 4f041384cb27f0d2. Unsoundness seems miraculously avoided by a safeguard I put in nativecode.ml. But other kernel changes in this commit should probably be reviewed carefully.
Diffstat (limited to 'kernel')
-rw-r--r--kernel/nativecode.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index eaddace4b..b17715a8f 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1849,9 +1849,10 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml =
and compile_rel env sigma univ auxdefs n =
let open Context.Rel in
- let n = length env.env_rel_context - n in
let open Declaration in
- match lookup n env.env_rel_context with
+ let decl = lookup n env.env_rel_context in
+ let n = length env.env_rel_context - n in
+ match decl with
| LocalDef (_,t,_) ->
let code = lambda_of_constr env sigma t in
let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in