diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-10-03 15:26:17 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-10-03 15:26:17 +0200 |
| commit | 6cc37a67e4be8e20cd3da46077ab8f3458e22394 (patch) | |
| tree | 7baf96eaccf037a94d7e525ccaec898955b465bd /kernel/nativecode.ml | |
| parent | 4a2e0798cf24c9edf4e96bd6ad62bdbde7a7cdf7 (diff) | |
| parent | d55818c7da468ce1c7c9644cb63f68f7561a17bc (diff) | |
Merge remote-tracking branch 'github/pr/263' into v8.6
Was PR#263: Fast lookup in named contexts
Diffstat (limited to 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index ad5b04f3d..eaddace4b 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1861,7 +1861,7 @@ and compile_rel env sigma univ auxdefs n = and compile_named env sigma univ auxdefs id = let open Context.Named.Declaration in - match Context.Named.lookup id env.env_named_context with + match lookup_named id env 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 |