From 7700051d09321735e27542676812194a2520b9fd 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.

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

diff --git a/prelude/tactics.v b/prelude/tactics.v
index cc6b86866..f0402a286 100644
--- 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 *)
-- 
GitLab