Backport PR #18393: Fixes #12755 and #18392: argument names wrongly s…

…hifted in nested sections

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).

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,19 +34,19 @@ 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,
   let r' = fst (subst_global subst r) in
   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

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 *)