From 3523794498e9ac8b86eeec8e1a2147e9abe997b6 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@inria.fr>
Date: Tue, 30 Jun 2020 13:33:39 +0200
Subject: Remove two axioms

---
 src/array/Array_checker.v | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'src/array/Array_checker.v')

diff --git a/src/array/Array_checker.v b/src/array/Array_checker.v
index 3a982b2..0540855 100644
--- a/src/array/Array_checker.v
+++ b/src/array/Array_checker.v
@@ -893,10 +893,6 @@ Section certif.
             apply read_over_other_write; now auto.
     Qed.
 
-  Axiom afold_left_or : forall a,
-    afold_left bool int false orb (Lit.interp rho) a =
-    C.interp rho (to_list a).
-
   Lemma valid_check_ext lres : C.valid rho (check_ext lres).
     unfold check_ext, eq_sel_sym.
     case_eq (Lit.is_pos lres); intro Heq; simpl; try now apply C.interp_true.
-- 
cgit