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.

2 files changed, 13 insertions, 1 deletions

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