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...

1 files 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}