Skip to content
Snippets Groups Projects
Commit ab1c4c33 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

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

parent 46e72edb
No related branches found
No related tags found
1 merge request!429Make sure that `naive_solver` does not create any new evars on leafs.
......@@ -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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment