diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-29 02:48:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-29 02:52:05 +0100 |
| commit | b2eaecf0e748e3c286e1ef337f72cee6d3475162 (patch) | |
| tree | d0924cca01d4f2f592c06706db010c975c5e08c4 /test-suite | |
| parent | 5122a39888cfc6afd2383d59465324dd67b69f4a (diff) | |
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.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/4462.v | 7 |
1 files changed, 7 insertions, 0 deletions
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). |