From 9f2ca1049957004161834090a697cd4118e2fb08 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 20 Jan 2015 14:54:48 +0100 Subject: Protect against redefinition of the __i64_xxx helper library functions. This is achieved by declaring these functions in C2C.ml, then re-checking their declarations in the global environment during the Selection pass. In passing, the "hf" parameter for SelectLong functions was removed and replaced by fixed identifiers corresponding to the actual names of the helper functions. --- extraction/extraction.v | 6 ------ 1 file changed, 6 deletions(-) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index ee496ffa..94ac6f52 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -57,12 +57,6 @@ Extract Constant Iteration.GenIter.iterate => (* Selection *) -Extract Constant SelectLong.get_helper => - "fun ge s sg -> - Errors.OK (Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s))". -Extract Constant SelectLong.get_builtin => - "fun s sg -> - Errors.OK (Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s))". Extract Constant Selection.compile_switch => "Switchaux.compile_switch". (* RTLgen *) -- cgit