diff options
| author | coqbot-app[bot] | 2021-01-11 13:55:52 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-11 13:55:52 +0000 |
| commit | 76de13a9ce03f542bca74dabee28bf27d9d8ac4f (patch) | |
| tree | 3907a1e6ec066f62871dcadc7a1350fa20173ee1 | |
| parent | ffb482f0c18bff2c65dcc9cd2b65bd20b398245d (diff) | |
| parent | 5c69eb442ac6b007854462066c38c3ec2556e311 (diff) | |
Merge PR #13622: Use the Evarutil cache for Class_tactics.evar_dependencies.
Reviewed-by: SkySkimmer
| -rw-r--r-- | tactics/class_tactics.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 9e66e8668f..d93501eea6 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1014,10 +1014,11 @@ let deps_of_constraints cstrs evm p = cstrs let evar_dependencies pred evm p = + let cache = Evarutil.create_undefined_evars_cache () in Evd.fold_undefined (fun ev evi _ -> if Evd.is_typeclass_evar evm ev && pred evm ev evi then - let evars = Evar.Set.add ev (Evarutil.undefined_evars_of_evar_info evm evi) + let evars = Evar.Set.add ev (Evarutil.filtered_undefined_evars_of_evar_info ~cache evm evi) in Intpart.union_set evars p else ()) evm () |