aboutsummaryrefslogtreecommitdiff
path: root/engine/evd.ml
diff options
context:
space:
mode:
authorWilliam Lawvere2017-07-01 22:10:46 -0700
committerWilliam Lawvere2017-07-01 22:10:46 -0700
commit80649ebaba75838bfd28ae78822cd2c078da4b23 (patch)
treeac29ab5edd3921dbee1c2256737347fd1542dc67 /engine/evd.ml
parentc2942e642ee6f83cc997f9a2510cdb7446a65cb4 (diff)
parent35e0f327405fb659c7ec5f9f7d26ea284aa45810 (diff)
Merge remote-tracking branch 'upstream/trunk' into trunk
Diffstat (limited to 'engine/evd.ml')
-rw-r--r--engine/evd.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index 08d26f40d4..bf1e052b63 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -659,8 +659,7 @@ let restrict evk filter ?candidates ?src evd =
let evar_info' =
{ evar_info with evar_filter = filter;
evar_candidates = candidates;
- evar_source = (match src with None -> evar_info.evar_source | Some src -> src);
- evar_extra = Store.empty } in
+ evar_source = (match src with None -> evar_info.evar_source | Some src -> src) } in
let last_mods = match evd.conv_pbs with
| [] -> evd.last_mods
| _ -> Evar.Set.add evk evd.last_mods in