From b6d58ca645f8f9c1023118b7a8a0208aa9a7f40b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 17 Jan 2018 00:39:19 +0100
Subject: [PATCH] Support `||` in `naive_solver`.
---
theories/tactics.v | 3 +++
1 file changed, 3 insertions(+)
diff --git a/theories/tactics.v b/theories/tactics.v
index 93c64f58..56dda3cd 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -517,6 +517,8 @@ Tactic Notation "naive_solver" tactic(tac) :=
| |- Is_true (_ && _) => apply andb_True; split
| H : _ ∨ _ |- _ =>
let H1 := fresh in destruct H as [H1|H1]; try clear H
+ | H : Is_true (_ || _) |- _ =>
+ apply orb_True in 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;
@@ -525,6 +527,7 @@ Tactic Notation "naive_solver" tactic(tac) :=
(**i instantiation of the conclusion *)
| |- ∃ x, _ => no_new_unsolved_evars ltac:(eexists; go n)
| |- _ ∨ _ => first [left; go n | right; go n]
+ | |- Is_true (_ || _) => apply orb_True; first [left; go n | right; go n]
| _ =>
(**i instantiations of assumptions. *)
lazymatch n with
--
GitLab