diff options
| author | Pierre-Marie Pédrot | 2018-10-27 14:04:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-27 14:04:32 +0200 |
| commit | 788ff535ed27d5142cd18878f8478bfc161945cd (patch) | |
| tree | cd513a51eaaa0ed5552c319cdc38b875bf7f2abc /vernac | |
| parent | be144dcaa1d1d8ff22e9e39f49fd247e813ac1f8 (diff) | |
| parent | fb1c2a017ef8112e061771db14ccc6cc1f09d41c (diff) | |
Merge PR #8741: [typeclasses] functionalize typeclass evar handling
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index a4b3a75c9f..ca77e03707 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -773,12 +773,13 @@ let pr_constraints printenv env sigma evars cstrs = let explain_unsatisfiable_constraints env sigma constr comp = let (_, constraints) = Evd.extract_all_conv_pbs sigma in + let tcs = Evd.get_typeclass_evars sigma in let undef = Evd.undefined_map sigma in (** Only keep evars that are subject to resolution and members of the given component. *) - let is_kept evk evi = match comp with - | None -> Typeclasses.is_resolvable evi - | Some comp -> Typeclasses.is_resolvable evi && Evar.Set.mem evk comp + let is_kept evk _ = match comp with + | None -> Evar.Set.mem evk tcs + | Some comp -> Evar.Set.mem evk tcs && Evar.Set.mem evk comp in let undef = let m = Evar.Map.filter is_kept undef in |