alternative implementation of mk_evar that keeps naive_solver working

This uses a hack to have side-effects in an ltac that returns a value.

Fixes #115 (closed)

tests/tactics.v

@@ -55,6 +55,11 @@ Proof. intros ?. rename select nat into m. exists m. done. Qed.
 Goal ∀ (P : nat → Prop), P 3 → P 4 → P 4.
 Proof. intros P **. rename select (P _) into HP4. apply HP4. Qed.
 
+(** Regression tests for [naive_solver]. *)
+Lemma naive_solver_issue_115 (P : nat → Prop) (x : nat) :
+  (∀ x', P x' → x' = 10) → P x → x + 1 = 11.
+Proof. naive_solver. Qed.
+
 (** [mk_evar] works on things that coerce to types. *)
 (** This is a feature when we have packed structures, for example Iris's [ofe]
 (fields other than the carrier omitted). *)
@@ -63,7 +68,6 @@ Goal ∀ A : ofe, True.
 intros A.
 let x := mk_evar A in idtac.
 Abort.
-
 (** More surprisingly, it also works for other coercions into a
 universe, like [Is_true : bool → Prop]. *)
 Goal True.