aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--pretyping/evd.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index fc4f5e040..632611291 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1385,7 +1385,7 @@ let set_metas evd metas = {
evar_names = evd.evar_names;
future_goals = evd.future_goals;
principal_future_goal = evd.principal_future_goal;
- extras = Store.empty;
+ extras = evd.extras;
}
let meta_list evd = metamap_to_list evd.metas