diff --git a/doc/changelog/02-specification-language/18393-master+fixes18392-12755-arguments-nested-section.rst b/doc/changelog/02-specification-language/18393-master+fixes18392-12755-arguments-nested-section.rst
new file mode 100644
index 000000000000..cd5dc0a01bfd
--- /dev/null
+++ b/doc/changelog/02-specification-language/18393-master+fixes18392-12755-arguments-nested-section.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  Wrong shift of argument names when using :cmd:`Arguments` in nested sections
+  (`#18393 <https://github.com/coq/coq/pull/18393>`_,
+  fixes `#12755 <https://github.com/coq/coq/issues/12755>`_
+  and `#18392 <https://github.com/coq/coq/issues/18392>`_,
+  by Hugo Herbelin).
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 8e8300cb8ae8..a1320178ac66 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -25,7 +25,7 @@ let name_table =
 
 type req =
   | ReqLocal
-  | ReqGlobal of GlobRef.t * Name.t list
+  | ReqGlobal
 
 let load_rename_args _ (_, (r, names)) =
   name_table := GlobRef.Map.add r names !name_table
@@ -34,7 +34,7 @@ let cache_rename_args o = load_rename_args 1 o
 
 let classify_rename_args = function
   | ReqLocal, _ -> Dispose
-  | ReqGlobal _, _ -> Substitute
+  | ReqGlobal, _ -> Substitute
 
 let subst_rename_args (subst, (_, (r, names as orig))) =
   ReqLocal,
@@ -42,11 +42,11 @@ let subst_rename_args (subst, (_, (r, names as orig))) =
   if r==r' then orig else (r', names)
 
 let discharge_rename_args = function
-  | ReqGlobal (c, names), _ as req when not (isVarRef c && Lib.is_in_section c) ->
+  | ReqGlobal, (c, names) as req when not (isVarRef c && Lib.is_in_section c) ->
      (try
        let var_names = Array.map_to_list (fun c -> Name (destVar c)) (Lib.section_instance c) in
-       let names' = var_names @ names in
-       Some (ReqGlobal (c, names), (c, names'))
+       let names = var_names @ names in
+       Some (ReqGlobal, (c, names))
      with Not_found -> Some req)
   | _ -> None
 
@@ -70,7 +70,7 @@ let rename_arguments local r names =
             ++ str" may not be renamed.")
     | _ -> ()
   in
-  let req = if local then ReqLocal else ReqGlobal (r, names) in
+  let req = if local then ReqLocal else ReqGlobal in
   Lib.add_leaf (inRenameArgs (req, (r, names)))
 
 let arguments_names r = GlobRef.Map.find r !name_table
diff --git a/test-suite/bugs/bug_12755.v b/test-suite/bugs/bug_12755.v
new file mode 100644
index 000000000000..1da792a6562b
--- /dev/null
+++ b/test-suite/bugs/bug_12755.v
@@ -0,0 +1,11 @@
+Section A.
+Context {a : nat}.
+Section B.
+Context {b : nat}.
+Definition foo (eq1 : a = a) (eq2 : b = b) (c : nat) : c = c := eq_refl.
+Global Arguments foo _ {_} {d} : rename.
+End B.
+End A.
+Arguments foo. (* was raising an anomaly *)
+Check foo _ (d:=0). (* was wrongly binding d to eq2 *)
+Fail Check foo (eq1 := 3) (eq_refl 2) (eq_refl 3) 4. (* was wrongly binding eq1 to b *)