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 /vernac | |
| parent | be144dcaa1d1d8ff22e9e39f49fd247e813ac1f8 (diff) | |
Cleanup evar_extra: remove evar_info's store and add maps to evar_map
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index a4b3a75c9f..50febdf448 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -776,9 +776,9 @@ let explain_unsatisfiable_constraints env sigma constr comp = 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 -> Evd.is_resolvable_evar sigma evk + | Some comp -> Evd.is_resolvable_evar sigma evk && Evar.Set.mem evk comp in let undef = let m = Evar.Map.filter is_kept undef in |