From f87c334f37dcc4230e6fb34933f53050ce8c1de8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 26 Jun 2019 08:53:40 +0200
Subject: [PATCH] Perform `fast_done` first in `naive_solver`.

This avoids `naive_solver` tearing whole goals apart, even if the goal
appears exactly as a hypothesis.
---
 theories/tactics.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/tactics.v b/theories/tactics.v
index 2fbf9234..bd85e7fd 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -506,6 +506,8 @@ Tactic Notation "naive_solver" tactic(tac) :=
   end;
   let rec go n :=
   repeat match goal with
+  (**i solve the goal *)
+  | |- _ => fast_done
   (**i intros *)
   | |- ∀ _, _ => intro
   (**i simplification of assumptions *)
@@ -522,8 +524,6 @@ Tactic Notation "naive_solver" tactic(tac) :=
   | H : Is_true (_ && _) |- _ => apply andb_True in H; destruct H
   (**i simplify and solve equalities *)
   | |- _ => progress simplify_eq/=
-  (**i solve the goal *)
-  | |- _ => fast_done
   (**i operations that generate more subgoals *)
   | |- _ ∧ _ => split
   | |- Is_true (bool_decide _) => apply (bool_decide_pack _)
-- 
GitLab