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 /plugins/ltac/rewrite.ml | |
| parent | be144dcaa1d1d8ff22e9e39f49fd247e813ac1f8 (diff) | |
Cleanup evar_extra: remove evar_info's store and add maps to evar_map
Diffstat (limited to 'plugins/ltac/rewrite.ml')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 9dd98a4ab7..8cecf9bd9b 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -89,9 +89,9 @@ let goalevars evars = fst evars let cstrevars evars = snd evars let new_cstr_evar (evd,cstrs) env t = - let s = Typeclasses.set_resolvable Evd.Store.empty false in - let (evd', t) = Evarutil.new_evar ~store:s env evd t in + let (evd', t) = Evarutil.new_evar env evd t in let ev, _ = destEvar evd' t in + let evd' = Evd.set_resolvable_evar evd' ev false in (evd', Evar.Set.add ev cstrs), t (** Building or looking up instances. *) |