diff options
| author | Matthieu Sozeau | 2018-10-08 02:14:07 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-10-26 18:29:36 +0200 |
| commit | 9f65b8bf9775dd571a806e10ac356b1b8f8ae2c5 (patch) | |
| tree | 56a49e0cd7d6ee19d4bb25ff0165e1c1466a7e73 /pretyping/typeclasses.mli | |
| parent | be144dcaa1d1d8ff22e9e39f49fd247e813ac1f8 (diff) | |
Cleanup evar_extra: remove evar_info's store and add maps to evar_map
Diffstat (limited to 'pretyping/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index f0437be4ed..de9a99a868 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -107,12 +107,9 @@ val no_goals_or_obligations : evar_filter An unresolvable evar is an evar the type-class engine will NOT try to solve *) -val set_resolvable : Evd.Store.t -> bool -> Evd.Store.t -val is_resolvable : evar_info -> bool -val mark_unresolvable : evar_info -> evar_info val mark_unresolvables : ?filter:evar_filter -> evar_map -> evar_map val mark_resolvables : ?filter:evar_filter -> evar_map -> evar_map -val mark_resolvable : evar_info -> evar_info + val is_class_evar : evar_map -> evar_info -> bool val is_class_type : evar_map -> EConstr.types -> bool |