diff --git a/dev/ci/user-overlays/18742-herbelin-master+one-copy-of-using-clause.sh b/dev/ci/user-overlays/18742-herbelin-master+one-copy-of-using-clause.sh
new file mode 100644
index 000000000000..ed391b0a28a4
--- /dev/null
+++ b/dev/ci/user-overlays/18742-herbelin-master+one-copy-of-using-clause.sh
@@ -0,0 +1 @@
+overlay elpi https://github.com/herbelin/coq-elpi coq-master+adapt-coq-pr18742-using-moved-from-cinfo-to-info 18742 master+one-copy-of-using-clause
diff --git a/test-suite/success/definition_using.v b/test-suite/success/definition_using.v
index ce89caafcba1..946a1265aba8 100644
--- a/test-suite/success/definition_using.v
+++ b/test-suite/success/definition_using.v
@@ -80,3 +80,43 @@ End B.
 Check c8 : forall a, c1 a = true -> bogus.
 Check c9 : forall a, c1 a = true -> bogus.
 Check c10: bogus -> bogus.
+
+Module TypeBehavior.
+
+Section S.
+Variables a : nat.
+#[using="Type", warning="-non-recursive"]
+Program Fixpoint b1 (n:nat) : nat := (fun _ => 0) a.
+Program Fixpoint b2 (n:nat) : (fun X _ => X) nat a := 0.
+Program Fixpoint b3 (n:nat) : (fun X _ => X) nat a := (fun _ => 0) a.
+Program Definition c1 : nat := (fun _ => 0) a.
+Program Definition c2 : (fun X _ => X) nat a := 0.
+Program Definition c3 : (fun X _ => X) nat a := (fun _ => 0) a.
+Fixpoint d1 (n:nat) : nat := (fun _ => 0) a.
+Fixpoint d2 (n:nat) : (fun X _ => X) nat a := 0.
+Fixpoint d3 (n:nat) : (fun X _ => X) nat a := (fun _ => 0) a.
+Definition e1 : nat := (fun _ => 0) a.
+Definition e2 : (fun X _ => X) nat a := 0.
+Definition e3 : (fun X _ => X) nat a := (fun _ => 0) a.
+End S.
+(* Not clear what is most expected below... *)
+
+(* Dependency in a with Program Fixpoint: the body is not reduced. *)
+Check b1 0 0 : nat.
+(* No dependency in a with Program Fixpoint, because both body and type are beta-reduced *)
+(* Why there is a difference with b1 is not clear *)
+Check b2 0 : nat.
+Check b3 0 : nat.
+(* With Program Definition, type is beta-reduced but not the body *)
+Check c1 0 : nat.
+Check c2 : nat.
+Check c3 0 : nat.
+(* With Definition/Fixpoint, neither body nor type are beta-reduced *)
+Check d1 0 0 : nat.
+Check d2 0 0 : nat.
+Check d3 0 0 : nat.
+Check e1 0 : nat.
+Check e2 0 : nat.
+Check e3 0 : nat.
+
+End TypeBehavior.
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
index adaa05ad061a..b98002667552 100644
--- a/test-suite/success/proof_using.v
+++ b/test-suite/success/proof_using.v
@@ -195,4 +195,61 @@ Qed.
 End Clear.
 *)
 
+Module InteractiveUsing.
 
+Section S.
+
+Variable m : nat.
+Variable e : m = m.
+
+#[using="e"]
+Definition a := 0.
+
+#[using="e"]
+Definition a' : nat.
+exact 0.
+Defined.
+
+#[using="e"]
+Fixpoint f (n:nat) : nat :=
+ match n with 0 => 0 | S n => f n end.
+
+#[using="e"]
+Fixpoint f' (n:nat) : nat.
+exact (match n with 0 => 0 | S n => f n end).
+Defined.
+
+#[using="Type"]
+Fixpoint f1 (n:nat) : nat :=
+  match n with 0 => 0 | S n => match f2 n with eq_refl => n end end
+with f2 (n:nat) : m = m :=
+  match n with 0 => eq_refl | S n => match f1 n with 0 => eq_refl | S _ => eq_refl end end.
+
+#[using="Type"]
+Fixpoint f1' (n:nat) : nat with f2' (n:nat) : m = m.
+exact (match n with 0 => 0 | S n => match f2' n with eq_refl => n end end).
+exact (match n with 0 => eq_refl | S n => match f1' n with 0 => eq_refl | S _ => eq_refl end end).
+Defined.
+
+CoInductive Stream : Set := Cons : Stream -> Stream.
+
+#[using="e"]
+CoFixpoint g : Stream := Cons g.
+
+#[using="e"]
+CoFixpoint g' : Stream.
+exact (Cons g).
+Defined.
+
+End S.
+
+Check eq_refl : a 0 (eq_refl 0) = 0.
+Check eq_refl : a' 0 (eq_refl 0) = 0.
+Check eq_refl : f 10 (eq_refl 10) 2 = 0.
+Check eq_refl : f' 10 (eq_refl 10) 2 = 0.
+Check eq_refl : f1 10 2 = 1.
+Check eq_refl : f1' 10 2 = 1.
+Check g 0 eq_refl : Stream.
+Check g' 0 eq_refl : Stream.
+
+End InteractiveUsing.
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index e9d9e76c058d..9bd593ef61f9 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -126,8 +126,8 @@ let do_definition ?hook ~name ?scope ?clearbody ~poly ?typing_flags ~kind ?using
   in
   let using = definition_using env evd ~body ~types ~using in
   let kind = Decls.IsDefinition kind in
-  let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types ?using () in
-  let info = Declare.Info.make ?scope ?clearbody ~kind ?hook ~udecl ~poly ?typing_flags ?user_warns () in
+  let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in
+  let info = Declare.Info.make ?scope ?clearbody ~kind ?hook ~udecl ~poly ?typing_flags ?user_warns ?using () in
   let _ : Names.GlobRef.t =
     Declare.declare_definition ~info ~cinfo ~opaque:false ~body evd
   in ()
@@ -151,7 +151,7 @@ let do_definition_program ?hook ~pm ~name ~scope ?clearbody ~poly ?typing_flags
   let using = definition_using env evd ~body ~types ~using in
   let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in
   let pm, _ =
-    let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in
-    let info = Declare.Info.make ~udecl ~scope ?clearbody ~poly ~kind ?hook ?typing_flags ?user_warns () in
+    let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
+    let info = Declare.Info.make ~udecl ~scope ?clearbody ~poly ~kind ?hook ?typing_flags ?user_warns ?using () in
     Declare.Obls.add_definition ~pm ~cinfo ~info ~term ~uctx obls
   in pm
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 8a37052f264f..add8df156fdd 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -259,39 +259,40 @@ let interp_fixpoint ?(check_recursivity=true) ?typing_flags ~cofix l :
   let uctx,fix = ground_fixpoint env evd fix in
   (fix,pl,uctx,info)
 
-let build_recthms ~indexes ?using fixnames fixtypes fiximps =
+let build_recthms ~indexes ?using fixnames fixdefs fixtypes fiximps =
   let fix_kind, cofix = match indexes with
     | Some indexes -> Decls.Fixpoint, false
     | None -> Decls.CoFixpoint, true
   in
   let thms =
     List.map3 (fun name typ (ctx,impargs,_) ->
-        let env = Global.env() in
-        let evd = Evd.from_env env in
-        let terms = [EConstr.of_constr typ] in
-        let using = Option.map (fun using -> Proof_using.definition_using env evd ~fixnames ~using ~terms) using in
         let args = List.map Context.Rel.Declaration.get_name ctx in
-        Declare.CInfo.make ~name ~typ ~args ~impargs ?using ()
+        Declare.CInfo.make ~name ~typ ~args ~impargs ()
       ) fixnames fixtypes fiximps
   in
-  fix_kind, cofix, thms
-
-let declare_fixpoint_interactive_generic ?indexes ~scope ?clearbody ~poly ?typing_flags ?user_warns ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns =
-  let fix_kind, cofix, thms = build_recthms ~indexes fixnames fixtypes fiximps in
+  let using =
+    let env = Global.env() in
+    let evd = Evd.from_env env in
+    let terms = List.map EConstr.of_constr (fixtypes @ List.map_filter (fun x -> x) fixdefs) in
+    Option.map (fun using -> Proof_using.definition_using env evd ~fixnames ~using ~terms) using in
+  fix_kind, cofix, thms, using
+
+let declare_fixpoint_interactive_generic ?indexes ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns =
+  let fix_kind, cofix, thms, using = build_recthms ~indexes ?using fixnames fixdefs fixtypes fiximps in
   let indexes = Option.default [] indexes in
   let init_terms = Some fixdefs in
   let evd = Evd.from_ctx ctx in
-  let info = Declare.Info.make ~poly ~scope ?clearbody ~kind:(Decls.IsDefinition fix_kind) ~udecl ?typing_flags ?user_warns ~ntns () in
+  let info = Declare.Info.make ~poly ~scope ?clearbody ~kind:(Decls.IsDefinition fix_kind) ~udecl ?typing_flags ?user_warns ~ntns ?using () in
   Declare.Proof.start_mutual_with_initialization ~info
     evd ~mutual_info:(cofix,indexes,init_terms) ~cinfo:thms None
 
 let declare_fixpoint_generic ?indexes ?scope ?clearbody ~poly ?typing_flags ?user_warns ?using ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
   (* We shortcut the proof process *)
-  let fix_kind, cofix, fixitems = build_recthms ~indexes ?using fixnames fixtypes fiximps in
+  let fix_kind, cofix, fixitems, using = build_recthms ~indexes ?using fixnames fixdefs fixtypes fiximps in
   let fixdefs = List.map Option.get fixdefs in
   let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
   let fix_kind = Decls.IsDefinition fix_kind in
-  let info = Declare.Info.make ?scope ?clearbody ~kind:fix_kind ~poly ~udecl ?typing_flags ?user_warns ~ntns () in
+  let info = Declare.Info.make ?scope ?clearbody ~kind:fix_kind ~poly ~udecl ?typing_flags ?user_warns ~ntns ?using () in
   let cinfo = fixitems in
   let _ : GlobRef.t list =
     Declare.declare_mutually_recursive ~cinfo ~info ~opaque:false ~uctx
@@ -331,9 +332,9 @@ let do_fixpoint_common ?typing_flags (fixl : Vernacexpr.fixpoint_expr list) =
   let (_, _, _, info as fix) = interp_fixpoint ~cofix:false ?typing_flags fixl in
   fixl, ntns, fix, List.map compute_possible_guardness_evidences info
 
-let do_fixpoint_interactive ~scope ?clearbody ~poly ?typing_flags ?user_warns l : Declare.Proof.t =
+let do_fixpoint_interactive ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using l : Declare.Proof.t =
   let fixl, ntns, fix, possible_indexes = do_fixpoint_common ?typing_flags l in
-  let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ?clearbody ~poly ?typing_flags ?user_warns fix ntns in
+  let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using fix ntns in
   lemma
 
 let do_fixpoint ?scope ?clearbody ~poly ?typing_flags ?user_warns ?using l =
@@ -345,9 +346,9 @@ let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) =
   let ntns = List.map_append (fun { Vernacexpr.notations } -> List.map Metasyntax.prepare_where_notation notations ) fixl in
   interp_fixpoint ~cofix:true fixl, ntns
 
-let do_cofixpoint_interactive ~scope ?clearbody ~poly ?typing_flags ?user_warns l =
+let do_cofixpoint_interactive ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using l =
   let cofix, ntns = do_cofixpoint_common l in
-  let lemma = declare_fixpoint_interactive_generic ~scope ?clearbody ~poly ?typing_flags ?user_warns cofix ntns in
+  let lemma = declare_fixpoint_interactive_generic ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using cofix ntns in
   lemma
 
 let do_cofixpoint ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using l =
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index d0152b8e5569..ca2458a06f69 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -21,6 +21,7 @@ val do_fixpoint_interactive
   -> poly:bool
   -> ?typing_flags:Declarations.typing_flags
   -> ?user_warns:UserWarn.t
+  -> ?using:Vernacexpr.section_subset_expr
   -> fixpoint_expr list
   -> Declare.Proof.t
 
@@ -40,6 +41,7 @@ val do_cofixpoint_interactive
   -> poly:bool
   -> ?typing_flags:Declarations.typing_flags
   -> ?user_warns:UserWarn.t
+  -> ?using:Vernacexpr.section_subset_expr
   -> cofixpoint_expr list
   -> Declare.Proof.t
 
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index e6feb4e47363..b3ef21e27e87 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -208,9 +208,9 @@ let build_wellfounded pm (recname,pl,bl,arityc,body) ?scope ?clearbody poly ?typ
     Option.map (fun using -> Proof_using.definition_using env sigma ~fixnames:[] ~using ~terms) using
   in
   let uctx = Evd.evar_universe_context sigma in
-  let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ ?using () in
+  let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ () in
   let kind = Decls.(IsDefinition Fixpoint) in
-  let info = Declare.Info.make ?scope ?clearbody ~kind ~poly ~udecl ~hook ?typing_flags ?user_warns ~ntns () in
+  let info = Declare.Info.make ?scope ?clearbody ~kind ~poly ~udecl ~hook ?typing_flags ?user_warns ?using ~ntns () in
   let pm, _ =
     Declare.Obls.add_definition ~pm ~cinfo ~info ~term:evars_def ~uctx evars in
   pm
@@ -237,20 +237,21 @@ let do_program_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?
   let (fixnames,fixrs,fixdefs,fixtypes) = fix in
   let collect_evars name def typ impargs =
     (* Generalize by the recursive prototypes  *)
-    let terms = [def; typ] in
-    let using = Option.map (fun using -> Proof_using.definition_using env evd ~fixnames ~using ~terms) using in
     let def = nf_evar evd (EConstr.it_mkNamedLambda_or_LetIn evd def rec_sign) in
     let typ = nf_evar evd (EConstr.it_mkNamedProd_or_LetIn evd typ rec_sign) in
     let deps = collect_evars_of_term evd def typ in
     let evars, _, def, typ =
       RetrieveObl.retrieve_obligations env name evd
         (List.length rec_sign) ~deps def typ in
-    let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in
+    let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
     (cinfo, def, evars)
   in
   let fiximps = List.map pi2 info in
   let fixdefs = List.map out_def fixdefs in
   let defs = List.map4 collect_evars fixnames fixdefs fixtypes fiximps in
+  let using =
+    let terms = fixdefs @ fixtypes in
+    Option.map (fun using -> Proof_using.definition_using env evd ~fixnames ~using ~terms) using in
   let () = if not cofix then begin
       let possible_indexes = List.map ComFixpoint.compute_possible_guardness_evidences info in
       (* XXX: are we allowed to have evars here? *)
@@ -278,7 +279,7 @@ let do_program_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?
   | Declare.Obls.IsCoFixpoint -> Decls.(IsDefinition CoFixpoint)
   in
   let ntns = List.map_append (fun { Vernacexpr.notations } -> List.map Metasyntax.prepare_where_notation notations ) fixl in
-  let info = Declare.Info.make ~poly ~scope ?clearbody ~kind ~udecl ?typing_flags ?user_warns ~ntns () in
+  let info = Declare.Info.make ~poly ~scope ?clearbody ~kind ~udecl ?typing_flags ?user_warns ~ntns ?using () in
   Declare.Obls.add_mutual_definitions ~pm defs ~info ~uctx fixkind
 
 let do_fixpoint ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using l =
diff --git a/vernac/declare.ml b/vernac/declare.ml
index f118235bdca4..0a508ba42d21 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -57,13 +57,11 @@ module CInfo = struct
     (** Names to pre-introduce  *)
     ; impargs : Impargs.manual_implicits
     (** Explicitily declared implicit arguments  *)
-    ; using : Proof_using.t option
-    (** Explicit declaration of section variables used by the constant *)
     }
 
 
-  let make ~name ~typ ?(args=[]) ?(impargs=[]) ?using () =
-    { name; typ; args; impargs; using }
+  let make ~name ~typ ?(args=[]) ?(impargs=[]) () =
+    { name; typ; args; impargs }
 
   let to_constr sigma thm = { thm with typ = EConstr.to_constr sigma thm.typ }
 
@@ -87,14 +85,16 @@ module Info = struct
     ; typing_flags : Declarations.typing_flags option
     ; user_warns : UserWarn.t option
     ; ntns : Metasyntax.notation_interpretation_decl list
+    ; using : Proof_using.t option
+    (** Explicit declaration of section variables used by the constant *)
     }
 
   (** Note that [opaque] doesn't appear here as it is not known at the
      start of the proof in the interactive case. *)
   let make ?(poly=false) ?(inline=false) ?(kind=Decls.(IsDefinition Definition))
       ?(udecl=UState.default_univ_decl) ?(scope=Locality.default_scope)
-      ?(clearbody=false) ?hook ?typing_flags ?user_warns ?(ntns=[]) () =
-    { poly; inline; kind; udecl; scope; hook; typing_flags; clearbody; user_warns; ntns }
+      ?(clearbody=false) ?hook ?typing_flags ?user_warns ?(ntns=[]) ?using () =
+    { poly; inline; kind; udecl; scope; hook; typing_flags; clearbody; user_warns; ntns; using }
 
 end
 
@@ -746,13 +746,13 @@ let mutual_make_bodies ~typing_flags ~fixitems ~rec_declaration ~possible_indexe
     vars, fixdecls, None
 
 let declare_mutually_recursive ~info ~cinfo ~opaque ~uctx ~rec_declaration ~possible_indexes =
-  let { Info.poly; udecl; scope; clearbody; kind; typing_flags; user_warns; ntns; _ } = info in
+  let { Info.poly; udecl; scope; clearbody; kind; typing_flags; user_warns; ntns; using; _ } = info in
   let vars, fixdecls, indexes =
     mutual_make_bodies ~typing_flags ~fixitems:cinfo ~rec_declaration ~possible_indexes in
   let uctx = UState.restrict uctx vars in
   let univs = UState.check_univ_decl ~poly uctx udecl in
   let csts = CList.map2
-      (fun CInfo.{ name; typ; impargs; using } body ->
+      (fun CInfo.{ name; typ; impargs } body ->
          let entry = definition_entry ~opaque ~types:typ ~univs ?using body in
          declare_entry ~name ~scope ~clearbody ~kind ~impargs ~uctx ~typing_flags ~user_warns entry)
       cinfo fixdecls
@@ -817,8 +817,8 @@ let prepare_definition ~info ~opaque ?using ~body ~typ sigma =
   entry, uctx
 
 let declare_definition_core ~info ~cinfo ~opaque ~obls ~body sigma =
-  let { CInfo.name; impargs; typ; using; _ } = cinfo in
-  let entry, uctx = prepare_definition ~info ~opaque ?using ~body ~typ sigma in
+  let { CInfo.name; impargs; typ; _ } = cinfo in
+  let entry, uctx = prepare_definition ~info ~opaque ?using:info.using ~body ~typ sigma in
   let { Info.scope; clearbody; kind; hook; typing_flags; user_warns; ntns; _ } = info in
   let gref = declare_entry_core ~name ~scope ~clearbody ~kind ~impargs ~typing_flags ~user_warns ~obls ?hook ~uctx entry in
   List.iter (Metasyntax.add_notation_interpretation ~local:(info.scope=Locality.Discharge) (Global.env ())) ntns;
@@ -952,7 +952,7 @@ module ProgramDecl = struct
     let set_uctx ~uctx prg = {prg with prg_uctx = uctx}
     let get_poly prg = prg.prg_info.Info.poly
     let get_obligations prg = prg.prg_obligations
-    let get_using prg = prg.prg_cinfo.CInfo.using
+    let get_using prg = prg.prg_info.Info.using
   end
 end
 
@@ -1274,7 +1274,7 @@ let declare_mutual_definition ~pm l =
     in
     let term = EConstr.to_constr sigma term in
     let typ = EConstr.to_constr sigma typ in
-    let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_cinfo.CInfo.impargs, x.prg_cinfo.CInfo.using) in
+    let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_cinfo.CInfo.impargs) in
     let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in
     (def, oblsubst)
   in
@@ -1288,11 +1288,11 @@ let declare_mutual_definition ~pm l =
   (*   let fixdefs = List.map reduce_fix fixdefs in *)
   let fixdefs, fixrs, fixtypes, fixitems =
     List.fold_right2
-      (fun (d, r, typ, impargs, using) name (a1, a2, a3, a4) ->
+      (fun (d, r, typ, impargs) name (a1, a2, a3, a4) ->
         ( d :: a1
         , r :: a2
         , typ :: a3
-        , (CInfo.make ~name ~typ ~impargs ?using ()) :: a4 ))
+        , (CInfo.make ~name ~typ ~impargs ()) :: a4 ))
       defs first.prg_deps ([], [], [], [])
   in
   let fixkind = Option.get first.prg_fixkind in
@@ -1536,7 +1536,6 @@ end
 
 type t =
   { endline_tactic : Genarg.glob_generic_argument option
-  ; using : Id.Set.t option
   ; proof : Proof.t
   ; initial_euctx : UState.t
   (** The initial universe context (for the statement) *)
@@ -1594,7 +1593,6 @@ let start_proof_core ~name ~typ ~pinfo ?(sign=initialize_named_context_for_proof
   let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
   { proof
   ; endline_tactic = None
-  ; using = None
   ; initial_euctx
   ; pinfo
   }
@@ -1619,7 +1617,6 @@ let start_dependent ~info ~name ~proof_ending goals =
   let pinfo = Proof_info.make ~info ~cinfo ~proof_ending () in
   { proof
   ; endline_tactic = None
-  ; using = None
   ; initial_euctx
   ; pinfo
   }
@@ -1692,7 +1689,7 @@ let start_mutual_with_initialization ~info ~cinfo ~mutual_info sigma snl =
       List.iter (Metasyntax.add_notation_interpretation ~local:(info.scope=Locality.Discharge) ntn_env) info.ntns in
     lemma
 
-let get_used_variables pf = pf.using
+let get_used_variables pf = pf.pinfo.Proof_info.info.Info.using
 let get_universe_decl pf = pf.pinfo.Proof_info.info.Info.udecl
 let get_recnames pf =
   if Option.has_some pf.pinfo.Proof_info.compute_guard then
@@ -1722,9 +1719,9 @@ let set_used_variables ps ~using =
        else (ctx, all_safe) in
   let ctx, _ =
     Environ.fold_named_context aux env ~init:(ctx,ctx_set) in
-  if not (Option.is_empty ps.using) then
+  if not (Option.is_empty ps.pinfo.info.using) then
     CErrors.user_err Pp.(str "Used section variables can be declared only once");
-  ctx, { ps with using = Some (Context.Named.to_vars ctx) }
+  ctx, { ps with pinfo = { ps.pinfo with info = { ps.pinfo.info with using = Some (Context.Named.to_vars ctx) } } }
 
 let get_open_goals ps =
   let Proof.{ goals; stack; sigma } = Proof.data ps.proof in
@@ -1848,8 +1845,8 @@ let make_univs ~poly ~uctx ~udecl eff (used_univs_typ, typ) (used_univs_body, bo
 
 let close_proof ?warn_incomplete ~opaque ~keep_body_ucst_separate ps =
 
-  let { using; proof; initial_euctx; pinfo } = ps in
-  let { Proof_info.info = { Info.udecl } } = pinfo in
+  let { proof; initial_euctx; pinfo } = ps in
+  let { Proof_info.info = { Info.udecl; using } } = pinfo in
   let { Proof.name; poly } = Proof.data proof in
   let unsafe_typ = keep_body_ucst_separate && not poly in
   let elist, uctx = prepare_proof ?warn_incomplete ~unsafe_typ ps in
@@ -1875,8 +1872,8 @@ let close_proof ?warn_incomplete ~opaque ~keep_body_ucst_separate ps =
 type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
 
 let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) =
-  let { using; proof; initial_euctx; pinfo } = ps in
-  let { Proof_info.info = { Info.udecl } } = pinfo in
+  let { proof; initial_euctx; pinfo } = ps in
+  let { Proof_info.info = { Info.udecl; using } } = pinfo in
   let { Proof.name; poly; entry; sigma } = Proof.data proof in
 
   (* We don't allow poly = true in this path *)
@@ -2509,9 +2506,9 @@ let solve_obligation ?check_final prg num tac =
     Proof_ending.End_obligation {name; num; auto; check_final}
   in
   let using = Internal.get_using prg in
-  let cinfo = CInfo.make ~name:obl.obl_name ~typ:(EConstr.of_constr obl.obl_type) ?using () in
+  let cinfo = CInfo.make ~name:obl.obl_name ~typ:(EConstr.of_constr obl.obl_type) () in
   let poly = Internal.get_poly prg in
-  let info = Info.make ~kind ~poly () in
+  let info = Info.make ~kind ~poly ?using () in
   let lemma = Proof.start_core ~cinfo ~info ~proof_ending evd  in
   let lemma = fst @@ Proof.by !default_tactic lemma in
   let lemma = Option.cata (fun tac -> Proof.set_endline_tactic tac lemma) lemma tac in
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 0999479fff30..96759b649f96 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -79,7 +79,6 @@ module CInfo : sig
     -> typ:'constr
     -> ?args:Name.t list
     -> ?impargs:Impargs.manual_implicits
-    -> ?using:Proof_using.t
     -> unit
     -> 'constr t
 
@@ -113,6 +112,7 @@ module Info : sig
     -> ?typing_flags:Declarations.typing_flags
     -> ?user_warns : UserWarn.t
     -> ?ntns : Metasyntax.notation_interpretation_decl list
+    -> ?using:Proof_using.t
     -> unit
     -> t
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 8e878e8a7f4e..6b69c0d0fd0b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -597,11 +597,6 @@ let vernac_set_used_variables pstate using : Declare.Proof.t =
   let _, pstate = Declare.Proof.set_used_variables pstate ~using in
   pstate
 
-let vernac_set_used_variables_opt ?using pstate =
-  match using with
-  | None -> pstate
-  | Some expr -> vernac_set_used_variables pstate expr
-
 (* XXX: Interpretation of lemma command, duplication with ComFixpoint
    / ComDefinition ? *)
 let interp_lemma ~program_mode ~flags ~scope env0 evd thms =
@@ -640,9 +635,11 @@ let start_lemma_com ~typing_flags ~program_mode ~poly ~scope ?clearbody ~kind ?u
   let evd, thms = interp_lemma ~program_mode ~flags ~scope env0 evd thms in
   let mut_analysis = RecLemmas.look_for_possibly_mutual_statements evd thms in
   let evd = Evd.minimize_universes evd in
-  let info = Declare.Info.make ?hook ~poly ~scope ?clearbody ~kind ~udecl ?typing_flags ?user_warns () in
-  begin
-    match mut_analysis with
+  let using =
+    let terms = List.map Declare.CInfo.get_typ thms in
+    Option.map (fun using -> Proof_using.definition_using env0 evd ~fixnames:[] ~using ~terms) using in
+  let info = Declare.Info.make ?hook ~poly ~scope ?clearbody ~kind ~udecl ?typing_flags ?user_warns ?using () in
+  match mut_analysis with
     | RecLemmas.NonMutual thm ->
       let thm = Declare.CInfo.to_constr evd thm in
       let evd = post_check_evd ~udecl ~poly evd in
@@ -651,9 +648,6 @@ let start_lemma_com ~typing_flags ~program_mode ~poly ~scope ?clearbody ~kind ?u
       let cinfo = List.map (Declare.CInfo.to_constr evd) cinfo in
       let evd = post_check_evd ~udecl ~poly evd in
       Declare.Proof.start_mutual_with_initialization ~info ~cinfo evd ~mutual_info (Some possible_guards)
-  end
-  (* XXX: This should be handled in start_with_initialization, see duplicate using in declare.ml *)
-  |> vernac_set_used_variables_opt ?using
 
 let vernac_definition_hook ~canonical_instance ~local ~poly ~reversible = let open Decls in function
 | Coercion ->
@@ -1066,8 +1060,7 @@ let vernac_fixpoint_interactive ~atts discharge l =
   if atts.program then
     CErrors.user_err Pp.(str"Program Fixpoint requires a body.");
   let typing_flags = atts.typing_flags in
-  ComFixpoint.do_fixpoint_interactive ~scope ?clearbody:atts.clearbody ~poly:atts.polymorphic ?typing_flags ?user_warns:atts.user_warns l
-  |> vernac_set_used_variables_opt ?using:atts.using
+  ComFixpoint.do_fixpoint_interactive ~scope ?clearbody:atts.clearbody ~poly:atts.polymorphic ?typing_flags ?user_warns:atts.user_warns ?using:atts.using l
 
 let vernac_fixpoint ~atts ~pm discharge l =
   let open DefAttributes in
@@ -1092,8 +1085,7 @@ let vernac_cofixpoint_interactive ~atts discharge l =
   let scope = vernac_cofixpoint_common ~atts discharge l in
   if atts.program then
     CErrors.user_err Pp.(str"Program CoFixpoint requires a body.");
-  vernac_set_used_variables_opt ?using:atts.using
-    (ComFixpoint.do_cofixpoint_interactive ~scope ~poly:atts.polymorphic l)
+  ComFixpoint.do_cofixpoint_interactive ~scope ~poly:atts.polymorphic ?using:atts.using l
 
 let vernac_cofixpoint ~atts ~pm discharge l =
   let open DefAttributes in