Merge branch 'robbert/naive_solver_evars' into 'master'

Make sure that `naive_solver` does not create any new evars on leafs.

Closes #163

See merge request !429

CHANGELOG.md

@@ -14,6 +14,8 @@ Coq 8.12 and 8.13 are no longer supported by this release.
   let `f_equiv` solve goals and subgoals of the form `R x x`. However, we use
   a restricted `fast_reflexivity` as full `reflexivity` can be quite expensive.
 - Rename `loopup_total_empty` -> `lookup_total_empty`.
+- Let `naive_solver tac` fail if `tac` creates new evars. Before it would
+  succeed with a proof that contains unresolved evars/shelved goals.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

stdpp/tactics.v

@@ -762,7 +762,7 @@ Tactic Notation "naive_solver" tactic(tac) :=
   | H : Is_true (_ || _) |- _ =>
      apply orb_True in H; let H1 := fresh in destruct H as [H1|H1]; try clear H
   (**i solve the goal using the user supplied tactic *)
-  | |- _ => solve [tac]
+  | |- _ => no_new_unsolved_evars (tac)
   end;
   (**i use recursion to enable backtracking on the following clauses. *)
   match goal with

tests/sets.v

-From stdpp Require Import sets.
+From stdpp Require Import sets gmap.
 
 Lemma foo `{Set_ A C} (x : A) (X Y : C) : x ∈ X ∩ Y → x ∈ X.
 Proof. intros Hx. set_unfold in Hx. tauto. Qed.
@@ -7,3 +7,7 @@ Proof. intros Hx. set_unfold in Hx. tauto. Qed.
 Lemma elem_of_list_bind_again {A B} (x : B) (l : list A) f :
   x ∈ l ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ l.
 Proof. set_solver. Qed.
+
+(** Should not leave any evars, see issue #163 *)
+Goal {[0]} ∪ dom (∅ : gmap nat nat) ≠ ∅.
+Proof. set_solver. Qed.