commit 5c94d0d375 breaks dependent evar line

[hendriktews]

Description of the problem

Commit 5c94d0d (Drop evar_concl from defined evars.) has the effect that the dependent evar line does not contain all existential variables any more. This breaks prooftrees functionality to track the status of existential variables.

The dependent evar line was reintroduced in PR #10489 as a response to feature request #10420.

In Coq before commit 5c94d0d the small Coq sample add below prints (dependent evars: ?X10:?n; in current goal:). After this commit one gets (dependent evars: ; in current goal:), which is wrong (at least with respect to feature request #10420), because ?n is still an open existential at that point, even though it does not appear in the current goal any more.

Small Coq file to reproduce the bug

Set Printing Dependent Evars Line.
Lemma x : (exists(n : nat), n = 5 \/ True) /\ (exists(m : nat), m = 6 \/ True).
Proof using.
  split.
    eexists.
    right.

Version of Coq where this bug occurs

8.18.0, 8.19, everything after 5c94d0d

Last version of Coq where the bug did not occur

8.17.1, everything before 5c94d0d

[SkySkimmer]

#18991

[hendriktews]

Thanks, I tested your PR, it works as expected on the example that I reported. However, there are still differences with respect to 8.17.1.
In the the following example

Set Printing Dependent Evars Line.

Section A.

  Variable fb : nat -> bool.
  Variable fp : nat -> Prop.
  Variable g : nat -> Prop.
  Hypothesis fb_fp : forall(n : nat), fb n = true <-> fp n.
  Hypothesis fp_g : forall(n : nat), fp n -> g n.

  Lemma a :
    forall(n : nat),
      fb n = true -> exists(m : nat), g m.
  Proof using fp_g fp fb_fp.
    intros n H.
    eexists.
    apply fb_fp in H.
    eauto.
  Qed.

after apply fb_fp 8.17 prints ?X8 using ?X14, meaning that ?X8 has been instanciated with a term containing the new evar ?x14. With your patch ?X8 simply vanishes.

[hendriktews]

IMO PR #18991 does not completely fix this issue, see my comment from yesterday.

[SkySkimmer]

The information isn't in the evar map anymore for that one AFAICT.