aboutsummaryrefslogtreecommitdiff
path: root/engine/evarutil.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/evarutil.ml')
-rw-r--r--engine/evarutil.ml7
1 files changed, 4 insertions, 3 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 5c2b480db4..96beb72a56 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -11,6 +11,7 @@
open CErrors
open Util
open Names
+open Context
open Constr
open Environ
open Evd
@@ -781,13 +782,13 @@ let cached_evar_of_hyp cache sigma decl accu = match cache with
in
NamedDecl.fold_constr fold decl accu
| Some cache ->
- let id = NamedDecl.get_id decl in
+ let id = NamedDecl.get_annot decl in
let r =
- try Id.Map.find id cache.cache
+ try Id.Map.find id.binder_name cache.cache
with Not_found ->
(* Dummy value *)
let r = ref (NamedDecl.LocalAssum (id, EConstr.mkProp), Evar.Set.empty) in
- let () = cache.cache <- Id.Map.add id r cache.cache in
+ let () = cache.cache <- Id.Map.add id.binder_name r cache.cache in
r
in
let (decl', evs) = !r in