Renamed arguments get misaligned after closing doubly nested sections

[jashug]

Description of the problem

When Global Arguments ... : rename is used within a section within another section, when the outer section is closed the names get messed up.

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.
About foo.
(*
foo : forall {b : nat}, a = a -> b = b -> forall c : nat, c = c
Arguments foo {b}%nat_scope eq1 eq2 d%nat_scope : rename
*)

End A.
About foo.
(*
foo : forall {a b : nat}, a = a -> b = b -> forall c : nat, c = c
Arguments foo {a eq1}%nat_scope eq2 d _%nat_scope : rename
*)

Check foo (eq1 := 3) (eq_refl 2) (eq_refl 3) 4.

See above how after End A the name b is dropped and all the names are shifted one place to the left.

Coq Version

Coq master 55f4095, but also appears to have existed for the past 9 years since the renaming feature was introduced in 39fd2b1.

Root cause

coq/pretyping/arguments_renaming.ml

Lines 46 to 51 in 55f4095

	| _, (ReqGlobal (c, names), _ as req) when not (isVarRef c && Lib.is_in_section c) ->
	(try
	let vars = Lib.variable_section_segment_of_reference c in
	let var_names = List.map (NamedDecl.get_id %> Name.mk_name) vars in
	let names' = var_names @ names in
	Some (ReqGlobal (c, names), (c, names'))

Here we only prepend the most recent section's variables to the list of original names.

[herbelin]

Fixed in #18393.