ssreflect: do not forget definedness of pre-existing evars

[Janno]

This is another LLM-generated change. The first commit fixes the original bug but that is too limited to be very useful. It only works if evars from src (i.e., those generated by open_constr) are instantiated solely by terms that are valid in dst.

The second commit fixes this shortcoming and is entirely beyond me.

Fixes / closes #13915

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.
  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

• Opened overlay pull requests.

[Janno]

@coqbot run full ci

[coqbot-app]

🔴 CI failures at commit 4641d8c without any failure in the test-suite

✔️ Corresponding jobs for the base commit 1d8273d succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-iris, ci-metarocq, ci-mtac2, ci-perennial

• You can also pass me a specific list of targets to minimize as arguments.

[Janno]

The iris failure is an aliasing bug that will be fixed in the next commit.

The unicoq failure is the same as the bug I am trying to fix. With evars x and y and 29 local definitions Hx := 29-x it runs:

  Time (apply: ((fun e: H1 + H2 + H3 + x = H4 + H5 + H6 + y => I) eq_refl)). (* ~2 secs. it is exponential *)
  Unshelve.
  - exact: 0.
  - exact: 1.

I suspect the last line doesn't do anything on master because there is no way the equation works with x:=0 and y:=1 (or vice versa).

Metarocq's erasure plugin is full of Unshelve. apply <something trivial>. Qed. so I guess they were also suffering from this bug.

[gares]

I'm only looking at the first commit, which makes sense to me.
But I would move the call to propagate before abs_evars_pirrel. Can we try that? Does it make the subsequent fix unneeded?