From 056068abd228fefab4951a61700aa6d54fb88287 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 29 Jan 2013 09:10:29 +0000 Subject: Ported to Coq 8.4pl1. Merge of branches/coq-8.4. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- extraction/extraction.v | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index 26cdb6d..89c708b 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -99,6 +99,15 @@ Extract Inlined Constant Fappli_IEEE.B2R => "fun _ -> assert false". Extract Inlined Constant Fappli_IEEE.round_mode => "fun _ -> assert false". Extract Inlined Constant Fcalc_bracket.inbetween_loc => "fun _ -> assert false". +(* Needed in Coq 4.00 to avoid problems with Function definitions. *) +Set Extraction AccessOpaque. + (* Go! *) Cd "extraction". -Recursive Extraction Library Compiler. +(* Recursive Extraction Library Compiler. *) +Separate Extraction + Compiler.transf_c_program Compiler.transf_cminor_program + Cexec.do_initial_state Cexec.do_step Cexec.at_final_state + Initializers.transl_init Initializers.constval + Csyntax.Eindex Csyntax.Epreincr. + -- cgit v1.2.3