Merge branch 'master' into merge_master_8.13.1

PARTIAL MERGE (PARTLY BROKEN).

See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE

WARNING:
 interface of va_args and assembly sections have changed

10 files changed, 80 insertions, 76 deletions

diff --git a/x86/Asm.v b/x86/Asm.v
index 33f1f2ad..799b533e 100644
--- a/x86/Asm.v
+++ b/x86/Asm.v
@@ -1193,7 +1193,7 @@ Ltac Equalities :=
   split. auto. intros. destruct B; auto. subst. auto.
 - (* trace length *)
   red; intros; inv H; simpl.
-  omega.
+  lia.
   eapply external_call_trace_length; eauto.
   eapply external_call_trace_length; eauto.
 - (* initial states *)
diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml
index 20f5d170..ecdf97f7 100644
--- a/x86/Asmexpand.ml
+++ b/x86/Asmexpand.ml
@@ -500,7 +500,7 @@ let expand_builtin_inline name args res =
    unprototyped. *)
 
 let fixup_funcall_elf64 sg =
-  if sg.sig_cc.cc_vararg || sg.sig_cc.cc_unproto then begin
+  if sg.sig_cc.cc_vararg <> None || sg.sig_cc.cc_unproto then begin
     let (ir, fr, ofs) = next_arg_locations 0 0 0 sg.sig_args in
     emit (Pmovl_ri (RAX, coqint_of_camlint (Int32.of_int fr)))
   end
@@ -521,7 +521,7 @@ let rec copy_fregs_to_iregs args fr ir =
       ()
 
 let fixup_funcall_win64 sg =
-  if sg.sig_cc.cc_vararg then
+  if sg.sig_cc.cc_vararg <> None then
     copy_fregs_to_iregs sg.sig_args [XMM0; XMM1; XMM2; XMM3] [RCX; RDX; R8; R9]
 
 let fixup_funcall sg =
diff --git a/x86/Asmgenproof.v b/x86/Asmgenproof.v
index 6886b2fd..8c28fb1b 100644
--- a/x86/Asmgenproof.v
+++ b/x86/Asmgenproof.v
@@ -67,7 +67,7 @@ Lemma transf_function_no_overflow:
   transf_function f = OK tf -> list_length_z (fn_code tf) <= Ptrofs.max_unsigned.
 Proof.
   intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x))); monadInv EQ0.
-  omega.
+  lia.
 Qed.
 
 Lemma exec_straight_exec:
@@ -332,8 +332,8 @@ Proof.
   split. unfold goto_label. rewrite P. rewrite H1. auto.
   split. rewrite Pregmap.gss. constructor; auto.
   rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q.
-  auto. omega.
-  generalize (transf_function_no_overflow _ _ H0). omega.
+  auto. lia.
+  generalize (transf_function_no_overflow _ _ H0). lia.
   intros. apply Pregmap.gso; auto.
 Qed.
 
@@ -858,7 +858,7 @@ Transparent destroyed_by_jumptable.
   econstructor; eauto.
   unfold nextinstr. rewrite Pregmap.gss. repeat rewrite Pregmap.gso; auto with asmgen.
   rewrite ATPC. simpl. constructor; eauto.
-  unfold fn_code. eapply code_tail_next_int. simpl in g. omega.
+  unfold fn_code. eapply code_tail_next_int. simpl in g. lia.
   constructor.
   apply agree_nextinstr. eapply agree_change_sp; eauto.
 Transparent destroyed_at_function_entry.
@@ -883,7 +883,7 @@ Transparent destroyed_at_function_entry.
 
 - (* return *)
   inv STACKS. simpl in *.
-  right. split. omega. split. auto.
+  right. split. lia. split. auto.
   econstructor; eauto. rewrite ATPC; eauto. congruence.
 Qed.
 
diff --git a/x86/ConstpropOpproof.v b/x86/ConstpropOpproof.v
index 82179fa4..09c6e91b 100644
--- a/x86/ConstpropOpproof.v
+++ b/x86/ConstpropOpproof.v
@@ -532,7 +532,7 @@ Proof.
   Int.bit_solve. destruct (zlt i0 n0).
   replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)).
   rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto.
-  rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto.
+  rewrite <- EQ. rewrite Int.bits_zero_ext by lia. rewrite zlt_true by auto.
   rewrite Int.bits_not by auto. apply negb_involutive.
   rewrite H6 by auto. auto.
   econstructor; split; eauto. auto.
diff --git a/x86/Conventions1.v b/x86/Conventions1.v
index b4cb233e..b6fb2620 100644
--- a/x86/Conventions1.v
+++ b/x86/Conventions1.v
@@ -303,14 +303,14 @@ Remark loc_arguments_32_charact:
   In p (loc_arguments_32 tyl ofs) -> forall_rpair (loc_argument_32_charact ofs) p.
 Proof.
   assert (X: forall ofs1 ofs2 l, loc_argument_32_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_32_charact ofs1 l).
-  { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. }
+  { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. }
   induction tyl as [ | ty tyl]; simpl loc_arguments_32; intros.
 - contradiction.
 - destruct H.
-+ destruct ty; subst p; simpl; omega.
++ destruct ty; subst p; simpl; lia.
 + apply IHtyl in H. generalize (typesize_pos ty); intros. destruct p; simpl in *.
-* eapply X; eauto; omega.
-* destruct H; split; eapply X; eauto; omega.
+* eapply X; eauto; lia.
+* destruct H; split; eapply X; eauto; lia.
 Qed.
 
 Remark loc_arguments_elf64_charact:
@@ -318,7 +318,7 @@ Remark loc_arguments_elf64_charact:
   In p (loc_arguments_elf64 tyl ir fr ofs) -> (2 | ofs) -> forall_rpair (loc_argument_elf64_charact ofs) p.
 Proof.
   assert (X: forall ofs1 ofs2 l, loc_argument_elf64_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_elf64_charact ofs1 l).
-  { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. }
+  { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. }
   assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_elf64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_elf64_charact ofs1) p).
   { destruct p; simpl; intuition eauto. }
   assert (Z: forall ofs, (2 | ofs) -> (2 | ofs + 2)).
@@ -335,8 +335,8 @@ Opaque list_nth_z.
   { intros. destruct (list_nth_z int_param_regs_elf64 ir) as [r|] eqn:E; destruct H1.
     subst. left. eapply list_nth_z_in; eauto.
     eapply IHtyl; eauto.
-    subst. split. omega. assumption.
-    eapply Y; eauto. omega. }
+    subst. split. lia. assumption.
+    eapply Y; eauto. lia. }
   assert (B: forall ty, In p
       match list_nth_z float_param_regs_elf64 fr with
       | Some ireg => One (R ireg) :: loc_arguments_elf64 tyl ir (fr + 1) ofs
@@ -346,8 +346,8 @@ Opaque list_nth_z.
   { intros. destruct (list_nth_z float_param_regs_elf64 fr) as [r|] eqn:E; destruct H1.
     subst. right. eapply list_nth_z_in; eauto.
     eapply IHtyl; eauto.
-    subst. split. omega. assumption.
-    eapply Y; eauto. omega. }
+    subst. split. lia. assumption.
+    eapply Y; eauto. lia. }
   destruct a; eauto.
 Qed.
 
@@ -356,7 +356,7 @@ Remark loc_arguments_win64_charact:
   In p (loc_arguments_win64 tyl r ofs) -> (2 | ofs) -> forall_rpair (loc_argument_win64_charact ofs) p.
 Proof.
   assert (X: forall ofs1 ofs2 l, loc_argument_win64_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_win64_charact ofs1 l).
-  { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. }
+  { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. }
   assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_win64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_win64_charact ofs1) p).
   { destruct p; simpl; intuition eauto. }
   assert (Z: forall ofs, (2 | ofs) -> (2 | ofs + 2)).
@@ -373,8 +373,8 @@ Opaque list_nth_z.
   { intros. destruct (list_nth_z int_param_regs_win64 r) as [r'|] eqn:E; destruct H1.
     subst. left. eapply list_nth_z_in; eauto.
     eapply IHtyl; eauto.
-    subst. split. omega. assumption.
-    eapply Y; eauto. omega. }
+    subst. split. lia. assumption.
+    eapply Y; eauto. lia. }
   assert (B: forall ty, In p
       match list_nth_z float_param_regs_win64 r with
       | Some ireg => One (R ireg) :: loc_arguments_win64 tyl (r + 1) ofs
@@ -384,8 +384,8 @@ Opaque list_nth_z.
   { intros. destruct (list_nth_z float_param_regs_win64 r) as [r'|] eqn:E; destruct H1.
     subst. right. eapply list_nth_z_in; eauto.
     eapply IHtyl; eauto.
-    subst. split. omega. assumption.
-    eapply Y; eauto. omega. }
+    subst. split. lia. assumption.
+    eapply Y; eauto. lia. }
   destruct a; eauto.
 Qed.
 
@@ -424,7 +424,7 @@ Proof.
   unfold forall_rpair; destruct p; intuition auto.
 Qed.
 
-Hint Resolve loc_arguments_acceptable: locs.
+Global Hint Resolve loc_arguments_acceptable: locs.
 
 Lemma loc_arguments_main:
   loc_arguments signature_main = nil.
@@ -432,7 +432,7 @@ Proof.
   unfold loc_arguments; destruct Archi.ptr64; auto; destruct Archi.win64; auto.
 Qed.
 
-(** ** Normalization of function results *)
+(** ** Normalization of function results and parameters *)
 
 (** In the x86 ABI, a return value of type "char" is returned in
     register AL, leaving the top 24 bits of EAX unspecified.
@@ -445,3 +445,8 @@ Definition return_value_needs_normalization (t: rettype) : bool :=
   | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => true
   | _ => false
   end.
+
+(** Function parameters are passed in normalized form and do not need
+    to be re-normalized at function entry. *)
+
+Definition parameter_needs_normalization (t: rettype) := false.
diff --git a/x86/NeedOp.v b/x86/NeedOp.v
index d9a58fbb..775a23db 100644
--- a/x86/NeedOp.v
+++ b/x86/NeedOp.v
@@ -206,9 +206,9 @@ Proof.
   unfold needs_of_operation; intros; destruct op; try (eapply default_needs_of_operation_sound; eauto; fail);
   simpl in *; FuncInv; InvAgree; TrivialExists.
 - apply sign_ext_sound; auto. compute; auto.
-- apply zero_ext_sound; auto. omega.
+- apply zero_ext_sound; auto. lia.
 - apply sign_ext_sound; auto. compute; auto.
-- apply zero_ext_sound; auto. omega.
+- apply zero_ext_sound; auto. lia.
 - apply neg_sound; auto.
 - apply mul_sound; auto.
 - apply mul_sound; auto with na.
@@ -246,10 +246,10 @@ Lemma operation_is_redundant_sound:
   vagree v arg1' nv.
 Proof.
   intros. destruct op; simpl in *; try discriminate; inv H1; FuncInv; subst.
-- apply sign_ext_redundant_sound; auto. omega.
-- apply zero_ext_redundant_sound; auto. omega.
-- apply sign_ext_redundant_sound; auto. omega.
-- apply zero_ext_redundant_sound; auto. omega.
+- apply sign_ext_redundant_sound; auto. lia.
+- apply zero_ext_redundant_sound; auto. lia.
+- apply sign_ext_redundant_sound; auto. lia.
+- apply zero_ext_redundant_sound; auto. lia.
 - apply andimm_redundant_sound; auto.
 - apply orimm_redundant_sound; auto.
 Qed.
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v
index af1d4e08..c43beb56 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -385,9 +385,9 @@ Proof.
 - TrivialExists. simpl. rewrite Int.and_commut; auto.
 - TrivialExists. simpl. rewrite Val.and_assoc. rewrite Int.and_commut. auto.
 - rewrite Val.zero_ext_and. TrivialExists. rewrite Val.and_assoc.
-  rewrite Int.and_commut. auto. omega.
+  rewrite Int.and_commut. auto. lia.
 - rewrite Val.zero_ext_and. TrivialExists. rewrite Val.and_assoc.
-  rewrite Int.and_commut. auto. omega.
+  rewrite Int.and_commut. auto. lia.
 - TrivialExists.
 Qed.
 
@@ -747,7 +747,7 @@ Proof.
   red; intros until x. unfold cast8unsigned. destruct (cast8unsigned_match a); intros; InvEval.
   TrivialExists.
   subst. rewrite Val.zero_ext_and. rewrite Val.and_assoc.
-  rewrite Int.and_commut. apply eval_andimm; auto. omega.
+  rewrite Int.and_commut. apply eval_andimm; auto. lia.
   TrivialExists.
 Qed.
 
@@ -763,7 +763,7 @@ Proof.
   red; intros until x. unfold cast16unsigned. destruct (cast16unsigned_match a); intros; InvEval.
   TrivialExists.
   subst. rewrite Val.zero_ext_and. rewrite Val.and_assoc.
-  rewrite Int.and_commut. apply eval_andimm; auto. omega.
+  rewrite Int.and_commut. apply eval_andimm; auto. lia.
   TrivialExists.
 Qed.
 
@@ -864,7 +864,7 @@ Proof.
   simpl. rewrite Heqo; reflexivity.
   simpl. unfold Int64.loword. rewrite Int64.unsigned_repr, Int.repr_unsigned; auto.
   assert (Int.modulus < Int64.max_unsigned) by reflexivity. 
-  generalize (Int.unsigned_range n); omega.
+  generalize (Int.unsigned_range n); lia.
 Qed.
 
 Theorem eval_floatofintu:
diff --git a/x86/Stacklayout.v b/x86/Stacklayout.v
index 4f68cf26..002b86bf 100644
--- a/x86/Stacklayout.v
+++ b/x86/Stacklayout.v
@@ -69,16 +69,16 @@ Local Opaque Z.add Z.mul sepconj range.
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
   set (oretaddr := align (ostkdata + b.(bound_stack_data)) w).
   replace (size_chunk Mptr) with w by (rewrite size_chunk_Mptr; auto).
-  assert (0 < w) by (unfold w; destruct Archi.ptr64; omega).
+  assert (0 < w) by (unfold w; destruct Archi.ptr64; lia).
   generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros.
-  assert (0 <= fe_ofs_arg) by (unfold fe_ofs_arg; destruct Archi.win64; omega).
-  assert (0 <= 4 * b.(bound_outgoing)) by omega.
-  assert (fe_ofs_arg + 4 * b.(bound_outgoing) <= olink) by (apply align_le; omega).
-  assert (olink + w <= ocs) by (unfold ocs; omega).
+  assert (0 <= fe_ofs_arg) by (unfold fe_ofs_arg; destruct Archi.win64; lia).
+  assert (0 <= 4 * b.(bound_outgoing)) by lia.
+  assert (fe_ofs_arg + 4 * b.(bound_outgoing) <= olink) by (apply align_le; lia).
+  assert (olink + w <= ocs) by (unfold ocs; lia).
   assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr).
-  assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega).
-  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega).
-  assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; omega).
+  assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia).
+  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; lia).
+  assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; lia).
 (* Reorder as:
      outgoing
      back link
@@ -90,13 +90,13 @@ Local Opaque Z.add Z.mul sepconj range.
   rewrite sep_swap45.
   rewrite sep_swap34.
 (* Apply range_split and range_split2 repeatedly *)
-  apply range_drop_left with 0. omega. 
-  apply range_split_2. fold olink. omega. omega.
-  apply range_split. omega.
-  apply range_split_2. fold ol. omega. omega.
-  apply range_drop_right with ostkdata. omega.
+  apply range_drop_left with 0. lia. 
+  apply range_split_2. fold olink. lia. lia.
+  apply range_split. lia.
+  apply range_split_2. fold ol. lia. lia.
+  apply range_drop_right with ostkdata. lia.
   rewrite sep_swap.
-  apply range_drop_left with (ostkdata + bound_stack_data b). omega.
+  apply range_drop_left with (ostkdata + bound_stack_data b). lia.
   rewrite sep_swap.
   exact H.
 Qed.
@@ -113,17 +113,17 @@ Proof.
   set (ol :=  align (size_callee_save_area b ocs) 8).
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
   set (oretaddr := align (ostkdata + b.(bound_stack_data)) w).
-  assert (0 < w) by (unfold w; destruct Archi.ptr64; omega).
+  assert (0 < w) by (unfold w; destruct Archi.ptr64; lia).
   generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros.
-  assert (0 <= fe_ofs_arg) by (unfold fe_ofs_arg; destruct Archi.win64; omega).
-  assert (0 <= 4 * b.(bound_outgoing)) by omega.
-  assert (fe_ofs_arg + 4 * b.(bound_outgoing) <= olink) by (apply align_le; omega).
-  assert (olink + w <= ocs) by (unfold ocs; omega).
+  assert (0 <= fe_ofs_arg) by (unfold fe_ofs_arg; destruct Archi.win64; lia).
+  assert (0 <= 4 * b.(bound_outgoing)) by lia.
+  assert (fe_ofs_arg + 4 * b.(bound_outgoing) <= olink) by (apply align_le; lia).
+  assert (olink + w <= ocs) by (unfold ocs; lia).
   assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr).
-  assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega).
-  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega).
-  assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; omega).
-  split. omega. omega.
+  assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia).
+  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; lia).
+  assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; lia).
+  split. lia. lia.
 Qed.
 
 Lemma frame_env_aligned:
@@ -142,11 +142,11 @@ Proof.
   set (ol :=  align (size_callee_save_area b ocs) 8).
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
   set (oretaddr := align (ostkdata + b.(bound_stack_data)) w).
-  assert (0 < w) by (unfold w; destruct Archi.ptr64; omega).
+  assert (0 < w) by (unfold w; destruct Archi.ptr64; lia).
   replace (align_chunk Mptr) with w by (rewrite align_chunk_Mptr; auto).
   split. exists (fe_ofs_arg / 8). unfold fe_ofs_arg; destruct Archi.win64; reflexivity.
-  split. apply align_divides; omega.
-  split. apply align_divides; omega.
-  split. apply align_divides; omega.
-  apply align_divides; omega.
+  split. apply align_divides; lia.
+  split. apply align_divides; lia.
+  split. apply align_divides; lia.
+  apply align_divides; lia.
 Qed.
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index 52955dcb..2000f96a 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -136,9 +136,9 @@ module ELF_System : SYSTEM =
       | Section_data(i, true) ->
          failwith "_Thread_local unsupported on this platform"
       | Section_data(i, false) | Section_small_data i ->
-          if i then ".data" else common_section ()
+          variable_section ~sec:".data" ~bss:".bss" i
       | Section_const i | Section_small_const i ->
-          if i || (not !Clflags.option_fcommon) then ".section	.rodata" else "COMM"
+          variable_section ~sec:".section	.rodata" i
       | Section_string -> ".section	.rodata"
       | Section_literal -> ".section	.rodata.cst8,\"aM\",@progbits,8"
       | Section_jumptable -> ".text"
@@ -233,11 +233,11 @@ module MacOS_System : SYSTEM =
       | Section_data(i, true) ->
          failwith "_Thread_local unsupported on this platform"
       | Section_data(i, false) | Section_small_data i ->
-          if i || (not !Clflags.option_fcommon) then ".data" else "COMM"
+          variable_section ~sec:".data" i
       | Section_const i  | Section_small_const i ->
-          if i || (not !Clflags.option_fcommon) then ".const" else "COMM"
+          variable_section ~sec:".const" ~reloc:".const_data" i
       | Section_string -> ".const"
-      | Section_literal -> ".literal8"
+      | Section_literal -> ".const"
       | Section_jumptable -> ".text"
       | Section_user(s, wr, ex) ->
           sprintf ".section	\"%s\", %s, %s"
@@ -297,9 +297,9 @@ module Cygwin_System : SYSTEM =
       | Section_data(i, true) ->
         failwith "_Thread_local unsupported on this platform"
       | Section_data(i, false) | Section_small_data i ->
-          if i then ".data" else common_section ()
+          variable_section ~sec:".data" ~bss:".bss" i
       | Section_const i | Section_small_const i ->
-          if i || (not !Clflags.option_fcommon) then ".section	.rdata,\"dr\"" else "COMM"
+          variable_section ~sec:".section	.rdata,\"dr\"" i
       | Section_string -> ".section	.rdata,\"dr\""
       | Section_literal -> ".section	.rdata,\"dr\""
       | Section_jumptable -> ".text"
@@ -796,7 +796,7 @@ module Target(System: SYSTEM):TARGET =
       | Pret ->
           if (not Archi.ptr64)
           && (!current_function_sig).sig_cc.cc_structret then begin
-            fprintf oc "	movl	0(%%esp), %%eax\n";
+            fprintf oc "	movl	4(%%esp), %%eax\n";
             fprintf oc "	ret	$4\n"
           end else begin
             fprintf oc "	ret\n"
@@ -979,8 +979,7 @@ module Target(System: SYSTEM):TARGET =
 
     let print_epilogue oc =
       if !need_masks then begin
-        section oc (Section_const true);
-        (* not Section_literal because not 8-bytes *)
+        section oc Section_literal;
         print_align oc 16;
         fprintf oc "%a:	.quad   0x8000000000000000, 0\n"
           raw_symbol "__negd_mask";
@@ -1010,7 +1009,7 @@ end
 let sel_target () =
  let module S = (val (match Configuration.system with
   | "linux" | "bsd" -> (module ELF_System:SYSTEM)
-  | "macosx" -> (module MacOS_System:SYSTEM)
+  | "macos" -> (module MacOS_System:SYSTEM)
   | "cygwin" -> (module Cygwin_System:SYSTEM)
   | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported")  ):SYSTEM) in
  (module Target(S):TARGET)
diff --git a/x86/extractionMachdep.v b/x86/extractionMachdep.v
index 20c6a521..614ec589 100644
--- a/x86/extractionMachdep.v
+++ b/x86/extractionMachdep.v
@@ -28,6 +28,6 @@ Extract Constant Archi.win64 =>
 
 Extract Constant SelectOp.symbol_is_external =>
   "match Configuration.system with
-    | ""macosx"" -> C2C.atom_is_extern
+    | ""macos"" -> C2C.atom_is_extern
     | ""cygwin"" when Archi.ptr64 -> C2C.atom_is_extern
     | _ -> (fun _ -> false)".