From 37ad0670e1dc02c47b4987c16602aadb462c44c2 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 23 Oct 2020 01:53:05 +0200 Subject: aarch64 compiles again (but ccomp generates incorrect assembly) --- extraction/extraction.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index bd396cd8..5de66797 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -13,6 +13,7 @@ (* *) (* *********************************************************************) +Require Import ZArith PeanoNat. Require Coqlib. Require Wfsimpl. Require DecidableClass Decidableplus. @@ -218,7 +219,8 @@ Set Extraction AccessOpaque. Cd "extraction". -Separate Extraction +Separate Extraction + Z.ldiff Z.lnot Nat.leb CSE3analysis.internal_analysis CSE3analysis.eq_depends_on_mem Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state -- cgit