diff --git a/theories/tactics.v b/theories/tactics.v
index cc6b86866622b8d5241686e079e35e68efb956fb..f0402a286c75a0ff9e7671710e54752bd95eed54 100644
--- a/theories/tactics.v
+++ b/theories/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 *)