diff options
| author | Pierre-Marie Pédrot | 2017-01-23 17:16:23 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-01-23 17:16:23 +0100 |
| commit | cfce4732363c7a93ffb7231335463d41c47074ea (patch) | |
| tree | 0aa35e11b13dddcfd0fd7029f02e72d8e7df5c0c /engine | |
| parent | e91ae93106b6bd6d92ef53ac18b04654485a8106 (diff) | |
| parent | a6f687852c0c7509a06fdf16c0af29129b3566d5 (diff) | |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index a6b6f742b7..c2f848291b 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -680,13 +680,16 @@ let restrict evk filter ?candidates evd = { evar_info with evar_filter = filter; evar_candidates = candidates; evar_extra = Store.empty } in + let last_mods = match evd.conv_pbs with + | [] -> evd.last_mods + | _ -> Evar.Set.add evk evd.last_mods in let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in let ctxt = Filter.filter_list filter (evar_context evar_info) in let id_inst = Array.map_of_list (mkVar % get_id) ctxt in let body = mkEvar(evk',id_inst) in let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in { evd with undf_evars = EvMap.add evk' evar_info' undf_evars; - defn_evars; evar_names }, evk' + defn_evars; last_mods; evar_names }, evk' let downcast evk ccl evd = let evar_info = EvMap.find evk evd.undf_evars in |