Merge PR #12033: Let coqdoc be informed by coq about binding variables (incidentally fixes #7697)

Reviewed-by: Lysxia

1 files changed, 1 insertions, 1 deletions

diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 1e2e2e53e2..43e86fa9bd 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -161,7 +161,7 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l =
     let env =
       EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (make_annot id r,t)) idl) env in
     let ienv = List.fold_right (fun {CAst.v=id} ienv ->
-      let impls = compute_internalization_data env sigma Variable t imps in
+      let impls = compute_internalization_data env sigma id Variable t imps in
       Id.Map.add id impls ienv) idl ienv in
       ((sigma,env,ienv),((is_coe,idl),t,imps)))
     (sigma,env,empty_internalization_env) l