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. --- test-suite/bugs/closed/4462.v | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 test-suite/bugs/closed/4462.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/4462.v b/test-suite/bugs/closed/4462.v new file mode 100644 index 000000000..c680518c6 --- /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