aboutsummaryrefslogtreecommitdiffstats
path: root/x86/extractionMachdep.v
diff options
context:
space:
mode:
Diffstat (limited to 'x86/extractionMachdep.v')
-rw-r--r--x86/extractionMachdep.v20
1 files changed, 12 insertions, 8 deletions
diff --git a/x86/extractionMachdep.v b/x86/extractionMachdep.v
index a29553e8..20c6a521 100644
--- a/x86/extractionMachdep.v
+++ b/x86/extractionMachdep.v
@@ -15,15 +15,19 @@
(* Additional extraction directives specific to the x86-64 port *)
-Require SelectOp ConstpropOp.
+Require Archi SelectOp.
-(* SelectOp *)
-
-Extract Constant SelectOp.symbol_is_external =>
- "fun id -> Configuration.system = ""macosx"" && C2C.atom_is_extern id".
+(* Archi *)
-(* ConstpropOp *)
+Extract Constant Archi.win64 =>
+ "match Configuration.system with
+ | ""cygwin"" when ptr64 -> true
+ | _ -> false".
-Extract Constant ConstpropOp.symbol_is_external =>
- "fun id -> Configuration.system = ""macosx"" && C2C.atom_is_extern id".
+(* SelectOp *)
+Extract Constant SelectOp.symbol_is_external =>
+ "match Configuration.system with
+ | ""macosx"" -> C2C.atom_is_extern
+ | ""cygwin"" when Archi.ptr64 -> C2C.atom_is_extern
+ | _ -> (fun _ -> false)".