Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10

1 files changed, 11 insertions, 0 deletions

diff --git a/src/QInst.v b/src/QInst.v
index 14ff0f7..8971380 100644
--- a/src/QInst.v
+++ b/src/QInst.v
@@ -74,6 +74,13 @@ Proof.
   destruct a; destruct c; intuition.
 Qed.
 
+Lemma eqb_or_split a b c:
+  Bool.eqb c (a || b) = true -> negb c || a || b = true.
+Proof.
+  intro H.
+  destruct a; destruct b; destruct c; intuition.
+Qed.
+
 (** verit considers equality modulo its symmetry, so we have to recover the
     right direction in the instances of the theorems *)
 (* TODO: currently incomplete *)
@@ -201,6 +208,10 @@ Ltac vauto :=
                          first [ strategy1 H
                                | strategy2 H ]
                        ]
+               | [ |- (negb ?A || ?B || ?C) = true ] =>
+                 eapply eqb_or_split;
+                 first [ strategy1 H
+                       | strategy2 H ]
                end
              ]
       );