Fix bug in naive_solver.

7700051d · Robbert Krebbers · 67246450 · 7700051d
Commit 7700051d authored Jan 12, 2016 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

prelude/tactics.v prelude/tactics.v +1 -1

No files found.
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -333,7 +333,7 @@ Tactic Notation "naive_solver" tactic(tac) :=
  | H : False |- _ => destruct H
  | H : _ ∧ _ |- _ => destruct H
  | H : ∃ _, _  |- _ => destruct H
-  | H : ?P → ?Q, H2 : ?Q |- _ => specialize (H H2)
+  | H : ?P → ?Q, H2 : ?P |- _ => specialize (H H2)
  (**i simplify and solve equalities *)
  | |- _ => progress simplify_equality'
  (**i solve the goal *)