aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evd.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-02-01 10:52:28 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-02-01 10:54:53 +0100
commitc17c3faee20251cd5c7168246e9ffcd12d557f85 (patch)
tree02635866b73d7595fad009cc17535a6bbf06c2fc /engine/evd.ml
parentf86bfa39cddfb9c6411ed8624cee9a2b5c8d53bd (diff)
parent568b38e1d599f8bac5adf140f5a114f2871bc436 (diff)
Merge branch 'v8.6'
Diffstat (limited to 'engine/evd.ml')
-rw-r--r--engine/evd.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index 7006fde3c..62d396395 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -681,13 +681,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 (NamedDecl.get_id %> mkVar) 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