naive_solver regression due to `mk_evar` tactic in !289

Require Import stdpp.prelude.

Lemma silly (P : nat → Prop) (x : nat) :
  (∀ x', P x' → x' = 10) → P x → x + 1 = 11.
Proof. naive_solver. Qed.

Used to work, fails after !289 (merged).

The above is a minimized example. Real problems in:

• LambdaRust: https://mattermost.mpi-sws.org/iris/pl/scfdqurmi3dhzmjs9qopeq76dc (discovered by @jung)
• Perennial: https://mattermost.mpi-sws.org/iris/pl/ca1cuwqztp8m7qfn61p9z8idey (discovered by @tchajed)

I noticed that using efeed by hand still works, but naive_solver calls it under no_new_unsolved_evars? Still unsure why mk_evar would break that.

Lemma silly (P : nat → Prop) (x : nat) :
  (∀ x', P x' → x' = 10) → P x → x + 1 = 11.
Proof.
  intros H1 H2.
  Fail naive_solver.
  efeed pose proof H1; naive_solver.
Qed.

I propose that we fix this by reverting the changes to efeed pose proof in !289 (merged), and later try to figure out how to fix mk_evar so that we can use it in efeed pose proof again. What do you think @jung?

Yeah makes sense.

Possibly to fix this we could use the more weird incantation for mk_evar... but that's a tactic that has side-effects and returns something, which Ltac really does not like. :/

mentioned in merge request !299 (merged)

mentioned in commit 7d502178

closed with merge request !299 (merged)