From cdab1f867c7c8d793c9727b31bf5fd7b5917b9d9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 22 Nov 2016 11:34:42 +0100
Subject: [PATCH] Patch naive_solver to deal with Coq bug #2901.

---
 theories/tactics.v | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/theories/tactics.v b/theories/tactics.v
index 6da40933..aa34f647 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -478,8 +478,12 @@ Tactic Notation "naive_solver" tactic(tac) :=
   | |- âˆ€ _, _ => intro
   (**i simplification of assumptions *)
   | H : False |- _ => destruct H
-  | H : _ âˆ§ _ |- _ => destruct H
-  | H : âˆƒ _, _  |- _ => destruct H
+  | H : _ âˆ§ _ |- _ =>
+     let H1 := fresh in let H2 := fresh in
+     destruct H as [H1 H2]; try clear H
+  | H : âˆƒ _, _  |- _ =>
+     let x := fresh in let Hx := fresh in
+     destruct H as [x Hx]; try clear H
   | H : ?P â†’ ?Q, H2 : ?P |- _ => specialize (H H2)
   | H : Is_true (bool_decide _) |- _ => apply (bool_decide_unpack _) in H
   | H : Is_true (_ && _) |- _ => apply andb_True in H; destruct H
@@ -491,7 +495,8 @@ Tactic Notation "naive_solver" tactic(tac) :=
   | |- _ âˆ§ _ => split
   | |- Is_true (bool_decide _) => apply (bool_decide_pack _)
   | |- Is_true (_ && _) => apply andb_True; split
-  | H : _ âˆ¨ _ |- _ => destruct H
+  | H : _ âˆ¨ _ |- _ =>
+     let H1 := fresh in destruct H as [H1|H1]; try clear H
   (**i solve the goal using the user supplied tactic *)
   | |- _ => solve [tac]
   end;
-- 
GitLab