From 28653f2963715936e828192a8e58794158c35ab6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 12 Jan 2016 14:27:47 +0100
Subject: [PATCH] Fix bug in naive_solver.

---
 theories/tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/tactics.v b/theories/tactics.v
index cc6b8686..f0402a28 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 *)
-- 
GitLab