diff options
| author | Gaëtan Gilbert | 2017-10-31 17:04:02 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 13:27:38 +0100 |
| commit | 23f84f37c674a07e925925b7e0d50d7ee8414093 (patch) | |
| tree | 7e470de5769c994d8df37c44fed12cf299d5b194 /engine/evarutil.ml | |
| parent | 75508769762372043387c67a9abe94e8f940e80a (diff) | |
Add relevance marks on binders.
Kernel should be mostly correct, higher levels do random stuff at
times.
Diffstat (limited to 'engine/evarutil.ml')
| -rw-r--r-- | engine/evarutil.ml | 7 |
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 |