From fa287eec3d57135ed1bd9285be0bc600449b13c1 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@inria.fr>
Date: Tue, 30 Jun 2020 16:09:52 +0200
Subject: Remove unused axiom

---
 src/bva/Bva_checker.v | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'src')

diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v
index 180fbcf..eebf5f9 100644
--- a/src/bva/Bva_checker.v
+++ b/src/bva/Bva_checker.v
@@ -1926,10 +1926,6 @@ Qed.
 Lemma eq_head: forall {A: Type} a b (l: list A), (a :: l) = (b :: l) <-> a = b.
 Proof. intros A a b l; split; [intros H; inversion H|intros ->]; auto. Qed.
 
-  Axiom afold_left_xor : forall a,
-    afold_left bool int false xorb (Lit.interp rho) a =
-    C.interp rho (to_list a).
-
 Lemma eqb_spec : forall x y, (x == y) = true <-> x = y.
 Proof.
  split;auto using eqb_correct, eqb_complete.
-- 
cgit