diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-05-02 11:34:53 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:59:01 +0200 |
| commit | 2de8910d2cc0af096e6d91b0ea165997ce144503 (patch) | |
| tree | 1e2345eea549fdc176f7abe17123a0be3051289b /pretyping/typeclasses.mli | |
| parent | ce11f55e27c8e4f98384aacd61ee67c593340195 (diff) | |
- Fix treatment of global universe constraints which should be passed along
in the Evd of proofs (Evd.from_env).
- Allow to set the Store.t value of new evars, e.g. to set constraint evars as
unresolvable in rewrite.ml.
- Fix a HUGE performance problem in the processing of constraints, which was remerging
all the previous constraints with the ambient global universes at each new constraint addition.
Performance is now back to (or better than) normal.
Diffstat (limited to 'pretyping/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index a8ce9ca7c..ebc6be45f 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -92,11 +92,12 @@ val no_goals_or_obligations : evar_filter (** Resolvability. Only undefined evars can be marked or checked for resolvability. *) +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 mark_resolvables : evar_map -> evar_map val is_class_evar : evar_map -> evar_info -> bool val resolve_typeclasses : ?filter:evar_filter -> ?split:bool -> ?fail:bool -> |