diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 50febdf448..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 _ = match comp with - | None -> Evd.is_resolvable_evar sigma evk - | Some comp -> Evd.is_resolvable_evar sigma evk && Evar.Set.mem evk comp + | 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 |