From b2eaecf0e748e3c286e1ef337f72cee6d3475162 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 Dec 2015 02:48:45 +0100
Subject: Fixing bug #4462: unshelve: Anomaly: Uncaught exception Not_found.

The rewrite tactic was causing an evar leak because of the use of the
Evd.remove primitive. This function did not modify the future goals of
the evarmap to remove the considered evar and thus maintained dangling
evars in there, causing the anomaly.
---
 pretyping/evd.ml              | 7 ++++++-
 test-suite/bugs/closed/4462.v | 7 +++++++
 2 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4462.v

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index c9b9f34414..8edc7a17c6 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -658,7 +658,12 @@ let add d e i = match i.evar_body with
 let remove d e =
   let undf_evars = EvMap.remove e d.undf_evars in
   let defn_evars = EvMap.remove e d.defn_evars in
-  { d with undf_evars; defn_evars; }
+  let principal_future_goal = match d.principal_future_goal with
+  | None -> None
+  | Some e' -> if Evar.equal e e' then None else d.principal_future_goal
+  in
+  let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in
+  { d with undf_evars; defn_evars; principal_future_goal; future_goals }
 
 let find d e =
   try EvMap.find e d.undf_evars
diff --git a/test-suite/bugs/closed/4462.v b/test-suite/bugs/closed/4462.v
new file mode 100644
index 0000000000..c680518c6a
--- /dev/null
+++ b/test-suite/bugs/closed/4462.v
@@ -0,0 +1,7 @@
+Variables P Q : Prop.
+Axiom pqrw : P <-> Q.
+
+Require Setoid.
+
+Goal P -> Q.
+unshelve (rewrite pqrw).
-- 
cgit v1.2.3