From 73c57090f7509e8d076ec7445278404ddc87f31e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 30 Dec 2013 17:02:36 +0100
Subject: When resetting an evarmap with the unsafe function
 Evd.evars_reset_evd with the flag with_conv_pbs, only reset the metas, not
 the last_mod field. It seemed strange to mix two unrelated things. This did
 not break anything visible...

---
 pretyping/evd.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 5870a22b73..1d084ac9bc 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -504,10 +504,8 @@ let has_undefined evd = not (EvMap.is_empty evd.undf_evars)
 
 let evars_reset_evd ?(with_conv_pbs=false) evd d =
   let conv_pbs = if with_conv_pbs then evd.conv_pbs else d.conv_pbs in
-  { evd with
-    metas = d.metas;
-    last_mods = d.last_mods;
-    conv_pbs; }
+  let last_mods = if with_conv_pbs then evd.last_mods else d.last_mods in
+  { evd with metas = d.metas; last_mods; conv_pbs; }
 
 let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs}
 
-- 
cgit v1.2.3