diff options
| author | Matthieu Sozeau | 2014-05-02 11:34:53 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:59:01 +0200 |
| commit | 2de8910d2cc0af096e6d91b0ea165997ce144503 (patch) | |
| tree | 1e2345eea549fdc176f7abe17123a0be3051289b /pretyping/typeclasses.ml | |
| 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.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index ada497ece7..8364387783 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -507,6 +507,9 @@ let is_implicit_arg = function let resolvable = Store.field () +let set_resolvable s b = + Store.set s resolvable b + let is_resolvable evi = assert (match evi.evar_body with Evar_empty -> true | _ -> false); Option.default true (Store.get evi.evar_extra resolvable) @@ -540,7 +543,7 @@ let mark_resolvability filter b sigma = Evd.raw_map_undefined map sigma let mark_unresolvables ?(filter=all_evars) sigma = mark_resolvability filter false sigma -let mark_resolvables sigma = mark_resolvability all_evars true sigma +let mark_resolvables ?(filter=all_evars) sigma = mark_resolvability filter true sigma let has_typeclasses filter evd = let check ev evi = |