diff options
| -rw-r--r-- | pretyping/evd.ml | 7 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4462.v | 7 |
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). |