diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-10 02:21:03 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-28 16:51:21 +0200 |
| commit | b772c323f62b322c9b0a4ab90c7de8b1e2066bae (patch) | |
| tree | 16dc8bc2ae1b5374a1329b9f6495d0a1b9905ee4 /pretyping/detyping.ml | |
| parent | d28304f6ba18ad9527a63cd01b39a5ad27526845 (diff) | |
Efficient computation of the names contained in an environment.
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index d81b88660..69a49749c 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -221,7 +221,7 @@ let lookup_name_as_displayed env sigma t s = | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c')) | Cast (c,_,_) -> lookup avoid n c | _ -> None - in lookup (Context.Named.to_vars (named_context env)) 1 t + in lookup (Environ.ids_of_named_context_val (Environ.named_context_val env)) 1 t let lookup_index_as_renamed env sigma t n = let rec lookup n d c = match EConstr.kind sigma c with |