From 39e45f296afefc936e3a63836d7f56c482ddee7a Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 12 Oct 2020 11:16:20 +0200
Subject: attribute #[using] for Definition and Fixpoint

---
 test-suite/success/definition_using.v | 46 ++++++++++++++++++
 vernac/attributes.ml                  |  8 +++
 vernac/attributes.mli                 |  1 +
 vernac/comDefinition.ml               | 16 ++++--
 vernac/comDefinition.mli              |  2 +
 vernac/comFixpoint.ml                 | 22 ++++++---
 vernac/comFixpoint.mli                |  4 +-
 vernac/comProgramFixpoint.ml          | 28 +++++++----
 vernac/comProgramFixpoint.mli         |  2 +
 vernac/declare.ml                     | 58 +++++++++++-----------
 vernac/declare.mli                    |  2 +
 vernac/g_vernac.mlg                   |  3 +-
 vernac/proof_using.ml                 | 26 +++++-----
 vernac/proof_using.mli                |  5 +-
 vernac/vernacentries.ml               | 91 ++++++++++++++++++++---------------
 15 files changed, 209 insertions(+), 105 deletions(-)
 create mode 100644 test-suite/success/definition_using.v

diff --git a/test-suite/success/definition_using.v b/test-suite/success/definition_using.v
new file mode 100644
index 0000000000..a8eab93404
--- /dev/null
+++ b/test-suite/success/definition_using.v
@@ -0,0 +1,46 @@
+Require Import Program.
+Axiom bogus : Type.
+
+Section A.
+Variable x : bogus.
+
+#[using="All"]
+Definition c1 : bool := true.
+
+#[using="All"]
+Fixpoint c2 n : bool :=
+  match n with
+  | O => true
+  | S p => c3 p
+  end
+with c3 n : bool :=
+  match n with
+  | O => true
+  | S p => c2 p
+end.
+
+#[using="All"]
+Definition c4 : bool. Proof. exact true. Qed.
+
+#[using="All"]
+Fixpoint c5 (n : nat) {struct n} : bool. Proof. destruct n as [|p]. exact true. exact (c5 p). Qed.
+
+#[using="All", program]
+Definition c6 : bool. Proof. exact true. Qed.
+
+#[using="All", program]
+Fixpoint c7 (n : nat) {struct n} : bool :=
+  match n with
+  | O => true
+  | S p => c7 p
+  end.
+
+End A.
+
+Check c1 : bogus -> bool.
+Check c2 : bogus -> nat -> bool.
+Check c3 : bogus -> nat -> bool.
+Check c4 : bogus -> bool.
+Check c5 : bogus -> nat -> bool.
+Check c6 : bogus -> bool.
+Check c7 : bogus -> nat -> bool.
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index fb308fd316..c55a7928d9 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -224,3 +224,11 @@ let canonical_field =
   enable_attribute ~key:"canonical" ~default:(fun () -> true)
 let canonical_instance =
   enable_attribute ~key:"canonical" ~default:(fun () -> false)
+
+let uses_parser : string key_parser = fun orig args ->
+  assert_once ~name:"using" orig;
+  match args with
+  | VernacFlagLeaf str -> str
+  |  _ -> CErrors.user_err (Pp.str "Ill formed uses attribute")
+
+let using = attribute_of_list ["using",uses_parser]
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 51bab79938..1969665082 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -51,6 +51,7 @@ val option_locality : Goptions.option_locality attribute
 val deprecation : Deprecation.t option attribute
 val canonical_field : bool attribute
 val canonical_instance : bool attribute
+val using : string option attribute
 
 val program_mode_option_name : string list
 (** For internal use when messing with the global option. *)
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index c1dbf0a1ea..aa71e58cf6 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -110,7 +110,7 @@ let interp_definition ~program_mode env evd impl_env bl red_option c ctypopt =
   let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in
   evd, (c, tyopt), imps
 
-let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
+let do_definition ?hook ~name ~scope ~poly ~kind ?using udecl bl red_option c ctypopt =
   let program_mode = false in
   let env = Global.env() in
   (* Explicitly bound universes and constraints *)
@@ -118,14 +118,18 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
   let evd, (body, types), impargs =
     interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt
   in
+  let using = using |> Option.map (fun expr ->
+    let terms = body :: match types with Some x -> [x] | None -> [] in
+    let l = Proof_using.process_expr (Global.env()) evd expr terms in
+    Names.Id.Set.(List.fold_right add l empty)) in
   let kind = Decls.IsDefinition kind in
-  let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in
+  let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types ?using () in
   let info = Declare.Info.make ~scope ~kind ?hook ~udecl ~poly () in
   let _ : Names.GlobRef.t =
     Declare.declare_definition ~info ~cinfo ~opaque:false ~body evd
   in ()
 
-let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
+let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind ?using udecl bl red_option c ctypopt =
   let program_mode = true in
   let env = Global.env() in
   (* Explicitly bound universes and constraints *)
@@ -133,9 +137,13 @@ let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind udecl bl red_option
   let evd, (body, types), impargs =
     interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt
   in
+  let using = using |> Option.map (fun expr ->
+    let terms = body :: match types with Some x -> [x] | None -> [] in
+    let l = Proof_using.process_expr (Global.env()) evd expr terms in
+    Names.Id.Set.(List.fold_right add l empty)) 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 () in
+    let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in
     let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook () in
     Declare.Obls.add_definition ~pm ~cinfo ~info ~term ~uctx obls
   in pm
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 7420235449..5e1b705ae4 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -31,6 +31,7 @@ val do_definition
   -> scope:Locality.locality
   -> poly:bool
   -> kind:Decls.definition_object_kind
+  -> ?using:Vernacexpr.section_subset_expr
   -> universe_decl_expr option
   -> local_binder_expr list
   -> red_expr option
@@ -45,6 +46,7 @@ val do_definition_program
   -> scope:Locality.locality
   -> poly:bool
   -> kind:Decls.logical_kind
+  -> ?using:Vernacexpr.section_subset_expr
   -> universe_decl_expr option
   -> local_binder_expr list
   -> red_expr option
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 78572c6aa6..bd11fa2b47 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -251,15 +251,21 @@ let interp_fixpoint ?(check_recursivity=true) ~cofix l :
   let uctx,fix = ground_fixpoint env evd fix in
   (fix,pl,uctx,info)
 
-let build_recthms ~indexes fixnames fixtypes fiximps =
+let build_recthms ~indexes ?using fixnames 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 using = using |> Option.map (fun expr ->
+          let terms = [EConstr.of_constr typ] in
+          let env = Global.env() in
+          let sigma = Evd.from_env env in
+          let l = Proof_using.process_expr env sigma expr terms in
+          Names.Id.Set.(List.fold_right add l empty)) in
         let args = List.map Context.Rel.Declaration.get_name ctx in
-        Declare.CInfo.make ~name ~typ ~args ~impargs ()
+        Declare.CInfo.make ~name ~typ ~args ~impargs ?using ()
       ) fixnames fixtypes fiximps
   in
   fix_kind, cofix, thms
@@ -277,9 +283,9 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   lemma
 
-let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
+let declare_fixpoint_generic ?indexes ~scope ~poly ?using ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
   (* We shortcut the proof process *)
-  let fix_kind, cofix, fixitems = build_recthms ~indexes fixnames fixtypes fiximps in
+  let fix_kind, cofix, fixitems = build_recthms ~indexes ?using fixnames 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
@@ -328,9 +334,9 @@ let do_fixpoint_interactive ~scope ~poly l : Declare.Proof.t =
   let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ~poly fix ntns in
   lemma
 
-let do_fixpoint ~scope ~poly l =
+let do_fixpoint ~scope ~poly ?using l =
   let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
-  declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns
+  declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly ?using fix ntns
 
 let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) =
   let fixl = List.map (fun fix -> {fix with Vernacexpr.rec_order = None}) fixl in
@@ -342,6 +348,6 @@ let do_cofixpoint_interactive ~scope ~poly l =
   let lemma = declare_fixpoint_interactive_generic ~scope ~poly cofix ntns in
   lemma
 
-let do_cofixpoint ~scope ~poly l =
+let do_cofixpoint ~scope ~poly ?using l =
   let cofix, ntns = do_cofixpoint_common l in
-  declare_fixpoint_generic ~scope ~poly cofix ntns
+  declare_fixpoint_generic ~scope ~poly ?using cofix ntns
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index aa5446205c..a36aba7672 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -19,13 +19,13 @@ val do_fixpoint_interactive :
   scope:Locality.locality -> poly:bool -> fixpoint_expr list -> Declare.Proof.t
 
 val do_fixpoint :
-  scope:Locality.locality -> poly:bool -> fixpoint_expr list -> unit
+  scope:Locality.locality -> poly:bool -> ?using:Vernacexpr.section_subset_expr -> fixpoint_expr list -> unit
 
 val do_cofixpoint_interactive :
   scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> Declare.Proof.t
 
 val do_cofixpoint :
-  scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> unit
+  scope:Locality.locality -> poly:bool -> ?using:Vernacexpr.section_subset_expr -> cofixpoint_expr list -> unit
 
 (************************************************************************)
 (** Internal API  *)
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 55901fd604..c2e07c4fd5 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -109,7 +109,7 @@ let telescope env sigma l =
 let nf_evar_context sigma ctx =
   List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx
 
-let build_wellfounded pm (recname,pl,bl,arityc,body) poly r measure notation =
+let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?using r measure notation =
   let open EConstr in
   let open Vars in
   let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
@@ -259,8 +259,12 @@ let build_wellfounded pm (recname,pl,bl,arityc,body) poly r measure notation =
   let evars, _, evars_def, evars_typ =
     RetrieveObl.retrieve_obligations env recname sigma 0 def typ
   in
+  let using = using |> Option.map (fun expr ->
+    let terms = List.map EConstr.of_constr [evars_def; evars_typ] in
+    let l = Proof_using.process_expr env sigma expr terms in
+    Names.Id.Set.(List.fold_right add l empty)) in
   let uctx = Evd.evar_universe_context sigma in
-  let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ () in
+  let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ ?using () in
   let info = Declare.Info.make ~udecl ~poly ~hook () in
   let pm, _ =
     Declare.Obls.add_definition ~pm ~cinfo ~info ~term:evars_def ~uctx evars in
@@ -275,7 +279,7 @@ let collect_evars_of_term evd c ty =
   Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
   evars (Evd.from_ctx (Evd.evar_universe_context evd))
 
-let do_program_recursive ~pm ~scope ~poly fixkind fixl =
+let do_program_recursive ~pm ~scope ~poly ?using fixkind fixl =
   let cofix = fixkind = Declare.Obls.IsCoFixpoint in
   let (env, rec_sign, udecl, evd), fix, info =
     interp_recursive ~cofix ~program_mode:true fixl
@@ -287,13 +291,17 @@ let do_program_recursive ~pm ~scope ~poly fixkind fixl =
   let evd = nf_evar_map_undefined evd in
   let collect_evars name def typ impargs =
     (* Generalize by the recursive prototypes  *)
+    let using = using |> Option.map (fun expr ->
+      let terms = [def; typ] in
+      let l = Proof_using.process_expr env evd expr terms in
+      Names.Id.Set.(List.fold_right add l empty)) in
     let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in
     let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in
     let evm = collect_evars_of_term evd def typ in
     let evars, _, def, typ =
       RetrieveObl.retrieve_obligations env name evm
         (List.length rec_sign) def typ in
-    let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
+    let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in
     (cinfo, def, evars)
   in
   let (fixnames,fixrs,fixdefs,fixtypes) = fix in
@@ -325,13 +333,13 @@ let do_program_recursive ~pm ~scope ~poly fixkind fixl =
   let info = Declare.Info.make ~poly ~scope ~kind ~udecl () in
   Declare.Obls.add_mutual_definitions ~pm defs ~info ~uctx ~ntns fixkind
 
-let do_fixpoint ~pm ~scope ~poly l =
+let do_fixpoint ~pm ~scope ~poly ?using l =
   let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in
     match g, l with
     | [Some { CAst.v = CWfRec (n,r) }],
       [ Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations} ] ->
         let recarg = mkIdentC n.CAst.v in
-        build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly r recarg notations
+        build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?using r recarg notations
 
     | [Some { CAst.v = CMeasureRec (n, m, r) }],
       [Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations }] ->
@@ -344,7 +352,7 @@ let do_fixpoint ~pm ~scope ~poly l =
           user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.")
         | _, _ -> r
       in
-        build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly
+        build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?using
           (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m notations
 
     | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g ->
@@ -352,11 +360,11 @@ let do_fixpoint ~pm ~scope ~poly l =
           Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in
       let fixkind = Declare.Obls.IsFixpoint annots in
       let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in
-      do_program_recursive ~pm ~scope ~poly fixkind l
+      do_program_recursive ~pm ~scope ~poly ?using fixkind l
     | _, _ ->
       CErrors.user_err ~hdr:"do_fixpoint"
         (str "Well-founded fixpoints not allowed in mutually recursive blocks")
 
-let do_cofixpoint ~pm ~scope ~poly fixl =
+let do_cofixpoint ~pm ~scope ~poly ?using fixl =
   let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in
-  do_program_recursive ~pm ~scope ~poly Declare.Obls.IsCoFixpoint fixl
+  do_program_recursive ~pm ~scope ~poly ?using Declare.Obls.IsCoFixpoint fixl
diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli
index 7935cf27fb..30bf3ae8f8 100644
--- a/vernac/comProgramFixpoint.mli
+++ b/vernac/comProgramFixpoint.mli
@@ -15,6 +15,7 @@ val do_fixpoint :
      pm:Declare.OblState.t
   -> scope:Locality.locality
   -> poly:bool
+  -> ?using:Vernacexpr.section_subset_expr
   -> fixpoint_expr list
   -> Declare.OblState.t
 
@@ -22,5 +23,6 @@ val do_cofixpoint :
      pm:Declare.OblState.t
   -> scope:Locality.locality
   -> poly:bool
+  -> ?using:Vernacexpr.section_subset_expr
   -> cofixpoint_expr list
   -> Declare.OblState.t
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 3a8ceb0e0f..0baae6eca5 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -55,11 +55,13 @@ module CInfo = struct
     (** Names to pre-introduce  *)
     ; impargs : Impargs.manual_implicits
     (** Explicitily declared implicit arguments  *)
+    ; using : Names.Id.Set.t option
+    (** Explicit declaration of section variables used by the constant *)
     }
 
 
-  let make ~name ~typ ?(args=[]) ?(impargs=[]) () =
-    { name; typ; args; impargs }
+  let make ~name ~typ ?(args=[]) ?(impargs=[]) ?using () =
+    { name; typ; args; impargs; using }
 
   let to_constr sigma thm = { thm with typ = EConstr.to_constr sigma thm.typ }
 
@@ -108,10 +110,10 @@ let default_univ_entry = Entries.Monomorphic_entry Univ.ContextSet.empty
 
 (** [univsbody] are universe-constraints attached to the body-only,
    used in vio-delayed opaque constants and private poly universes *)
-let definition_entry_core ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types
+let definition_entry_core ?(opaque=false) ?using ?(inline=false) ?feedback_id ?types
     ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body =
   { proof_entry_body = Future.from_val ((body,univsbody), eff);
-    proof_entry_secctx = section_vars;
+    proof_entry_secctx = using;
     proof_entry_type = types;
     proof_entry_universes = univs;
     proof_entry_opaque = opaque;
@@ -119,7 +121,7 @@ let definition_entry_core ?(opaque=false) ?(inline=false) ?feedback_id ?section_
     proof_entry_inline_code = inline}
 
 let definition_entry =
-  definition_entry_core ?eff:None ?univsbody:None ?feedback_id:None ?section_vars:None
+  definition_entry_core ?eff:None ?univsbody:None ?feedback_id:None
 
 type 'a constant_entry =
   | DefinitionEntry of 'a proof_entry
@@ -236,9 +238,9 @@ let pure_definition_entry ?(opaque=false) ?(inline=false) ?types
     proof_entry_feedback = None;
     proof_entry_inline_code = inline}
 
-let delayed_definition_entry ~opaque ?feedback_id ~section_vars ~univs ?types body =
+let delayed_definition_entry ~opaque ?feedback_id ~using ~univs ?types body =
   { proof_entry_body = body
-  ; proof_entry_secctx = section_vars
+  ; proof_entry_secctx = using
   ; proof_entry_type = types
   ; proof_entry_universes = univs
   ; proof_entry_opaque = opaque
@@ -608,8 +610,8 @@ let declare_mutually_recursive_core ~info ~cinfo ~opaque ~ntns ~uctx ~rec_declar
       uctx, univs
   in
   let csts = CList.map2
-      (fun CInfo.{ name; typ; impargs } body ->
-         let entry = definition_entry ~opaque ~types:typ ~univs body in
+      (fun CInfo.{ name; typ; impargs; using } body ->
+         let entry = definition_entry ~opaque ~types:typ ~univs ?using body in
          declare_entry ~name ~scope ~kind ~impargs ~uctx entry)
       cinfo fixdecls
   in
@@ -660,7 +662,7 @@ let check_evars_are_solved env sigma t =
   let evars = Evarutil.undefined_evars_of_term sigma t in
   if not (Evar.Set.is_empty evars) then error_unresolved_evars env sigma t evars
 
-let prepare_definition ~info ~opaque ~body ~typ sigma =
+let prepare_definition ~info ~opaque ?using ~body ~typ sigma =
   let { Info.poly; udecl; inline; _ } = info in
   let env = Global.env () in
   let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false
@@ -669,13 +671,13 @@ let prepare_definition ~info ~opaque ~body ~typ sigma =
   Option.iter (check_evars_are_solved env sigma) types;
   check_evars_are_solved env sigma body;
   let univs = Evd.check_univ_decl ~poly sigma udecl in
-  let entry = definition_entry ~opaque ~inline ?types ~univs body in
+  let entry = definition_entry ~opaque ?using ~inline ?types ~univs body in
   let uctx = Evd.evar_universe_context sigma in
   entry, uctx
 
 let declare_definition_core ~info ~cinfo ~opaque ~obls ~body sigma =
-  let { CInfo.name; impargs; typ; _ } = cinfo in
-  let entry, uctx = prepare_definition ~info ~opaque ~body ~typ sigma in
+  let { CInfo.name; impargs; typ; using; _ } = cinfo in
+  let entry, uctx = prepare_definition ~info ~opaque ?using ~body ~typ sigma in
   let { Info.scope; kind; hook; _ } = info in
   declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry, uctx
 
@@ -803,6 +805,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
   end
 end
 
@@ -1137,7 +1140,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) in
+    let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_cinfo.CInfo.impargs, x.prg_cinfo.CInfo.using) in
     let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in
     (def, oblsubst)
   in
@@ -1151,11 +1154,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) name (a1, a2, a3, a4) ->
+      (fun (d, r, typ, impargs, using) name (a1, a2, a3, a4) ->
         ( d :: a1
         , r :: a2
         , typ :: a3
-        , CInfo.{name; typ; impargs; args = []} :: a4 ))
+        , CInfo.{name; typ; impargs; args = []; using } :: a4 ))
       defs first.prg_deps ([], [], [], [])
   in
   let fixkind = Option.get first.prg_fixkind in
@@ -1376,7 +1379,7 @@ end
 
 type t =
   { endline_tactic : Genarg.glob_generic_argument option
-  ; section_vars : Id.Set.t option
+  ; using : Id.Set.t option
   ; proof : Proof.t
   ; initial_euctx : UState.t
   (** The initial universe context (for the statement) *)
@@ -1435,7 +1438,7 @@ 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
-  ; section_vars = None
+  ; using = None
   ; initial_euctx
   ; pinfo
   }
@@ -1458,7 +1461,7 @@ let start_dependent ~info ~name ~proof_ending goals =
   let pinfo = Proof_info.make ~info ~cinfo ~proof_ending () in
   { proof
   ; endline_tactic = None
-  ; section_vars = None
+  ; using = None
   ; initial_euctx
   ; pinfo
   }
@@ -1523,7 +1526,7 @@ let start_mutual_with_initialization ~info ~cinfo ~mutual_info sigma snl =
     map lemma ~f:(fun p ->
         pi1 @@ Proof.run_tactic Global.(env ()) init_tac p)
 
-let get_used_variables pf = pf.section_vars
+let get_used_variables pf = pf.using
 let get_universe_decl pf = pf.pinfo.Proof_info.info.Info.udecl
 
 let set_used_variables ps l =
@@ -1547,9 +1550,9 @@ let set_used_variables ps l =
        else (ctx, all_safe) in
   let ctx, _ =
     Environ.fold_named_context aux env ~init:(ctx,ctx_set) in
-  if not (Option.is_empty ps.section_vars) then
+  if not (Option.is_empty ps.using) then
     CErrors.user_err Pp.(str "Used section variables can be declared only once");
-  ctx, { ps with section_vars = Some (Context.Named.to_vars ctx) }
+  ctx, { ps with using = Some (Context.Named.to_vars ctx) }
 
 let get_open_goals ps =
   let Proof.{ goals; stack; sigma } = Proof.data ps.proof in
@@ -1646,7 +1649,7 @@ let make_univs ~poly ~uctx ~udecl (used_univs_typ, typ) (used_univs_body, body)
 
 let close_proof ~opaque ~keep_body_ucst_separate ps =
 
-  let { section_vars; proof; initial_euctx; pinfo } = ps in
+  let { using; proof; initial_euctx; pinfo } = ps in
   let { Proof_info.info = { Info.udecl } } = pinfo in
   let { Proof.name; poly } = Proof.data proof in
   let unsafe_typ = keep_body_ucst_separate && not poly in
@@ -1667,7 +1670,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
       then make_univs_private_poly ~poly ~uctx ~udecl t b
       else make_univs ~poly ~uctx ~udecl t b
     in
-    definition_entry_core ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
+    definition_entry_core ~opaque ?using ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
   in
   let entries = CList.map make_entry elist  in
   { name; entries; uctx }
@@ -1675,7 +1678,7 @@ let close_proof ~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 { section_vars; proof; initial_euctx; pinfo } = ps in
+  let { using; proof; initial_euctx; pinfo } = ps in
   let { Proof_info.info = { Info.udecl } } = pinfo in
   let { Proof.name; poly; entry; sigma } = Proof.data proof in
 
@@ -1712,7 +1715,7 @@ let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.comput
         let univs = UState.restrict uctx used_univs in
         let univs = UState.check_mono_univ_decl univs udecl in
         (pt,univs),eff)
-    |> delayed_definition_entry ~opaque ~feedback_id ~section_vars ~univs ~types
+    |> delayed_definition_entry ~opaque ~feedback_id ~using ~univs ~types
   in
   let entries = Future.map2 make_entry fpl (Proofview.initial_goals entry) in
   { name; entries; uctx = initial_euctx }
@@ -2289,7 +2292,8 @@ let rec solve_obligation prg num tac =
     let name = Internal.get_name prg in
     Proof_ending.End_obligation {name; num; auto}
   in
-  let cinfo = CInfo.make ~name:obl.obl_name ~typ:(EConstr.of_constr obl.obl_type) () 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 poly = Internal.get_poly prg in
   let info = Info.make ~scope ~kind ~poly () in
   let lemma = Proof.start_core ~cinfo ~info ~proof_ending evd  in
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 1ad79928d5..4f86dd472b 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -79,6 +79,7 @@ module CInfo : sig
     -> typ:'constr
     -> ?args:Name.t list
     -> ?impargs:Impargs.manual_implicits
+    -> ?using:Names.Id.Set.t
     -> unit
     -> 'constr t
 
@@ -333,6 +334,7 @@ type 'a proof_entry
 
 val definition_entry
   :  ?opaque:bool
+  -> ?using:Names.Id.Set.t
   -> ?inline:bool
   -> ?types:Constr.types
   -> ?univs:Entries.universes_entry
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3d6a93c888..f192d67624 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -113,7 +113,8 @@ GRAMMAR EXTEND Gram
     ]
   ;
   attribute:
-    [ [ k = ident ; v = attr_value -> { Names.Id.to_string k, v } ]
+    [ [ k = ident ; v = attr_value -> { Names.Id.to_string k, v }
+      | "using" ; v = attr_value -> { "using", v } ]
     ]
   ;
   attr_value:
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index 95680c2a4e..bdb0cabacf 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -18,30 +18,30 @@ module NamedDecl = Context.Named.Declaration
 
 let known_names = Summary.ref [] ~name:"proofusing-nameset"
 
-let rec close_fwd e s =
+let rec close_fwd env sigma s =
   let s' =
     List.fold_left (fun s decl ->
       let vb = match decl with
                | LocalAssum _ -> Id.Set.empty
-               | LocalDef (_,b,_) -> global_vars_set e b
+               | LocalDef (_,b,_) -> Termops.global_vars_set env sigma b
       in
-      let vty = global_vars_set e (NamedDecl.get_type decl) in
+      let vty = Termops.global_vars_set env sigma (NamedDecl.get_type decl) in
       let vbty = Id.Set.union vb vty in
       if Id.Set.exists (fun v -> Id.Set.mem v s) vbty
       then Id.Set.add (NamedDecl.get_id decl) (Id.Set.union s vbty) else s)
-    s (named_context e)
+    s (EConstr.named_context env)
     in
-  if Id.Set.equal s s' then s else close_fwd e s'
+  if Id.Set.equal s s' then s else close_fwd env sigma s'
 
-let set_of_type env ty =
+let set_of_type env sigma ty =
   List.fold_left (fun acc ty ->
-      Id.Set.union (global_vars_set env ty) acc)
+      Id.Set.union (Termops.global_vars_set env sigma ty) acc)
     Id.Set.empty ty
 
 let full_set env =
   List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty
 
-let process_expr env e v_ty =
+let process_expr env sigma e v_ty =
   let rec aux = function
     | SsEmpty -> Id.Set.empty
     | SsType -> v_ty
@@ -49,7 +49,7 @@ let process_expr env e v_ty =
     | SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2)
     | SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2)
     | SsCompl e -> Id.Set.diff (full_set env) (aux e)
-    | SsFwdClose e -> close_fwd env (aux e)
+    | SsFwdClose e -> close_fwd env sigma (aux e)
   and set_of_id id =
     if Id.to_string id = "All" then
       full_set env
@@ -59,9 +59,9 @@ let process_expr env e v_ty =
   in
   aux e
 
-let process_expr env e ty =
-  let v_ty = set_of_type env ty in
-  let s = Id.Set.union v_ty (process_expr env e v_ty) in
+let process_expr env sigma e ty =
+  let v_ty = set_of_type env sigma ty in
+  let s = Id.Set.union v_ty (process_expr env sigma e v_ty) in
   Id.Set.elements s
 
 let name_set id expr = known_names := (id,expr) :: !known_names
@@ -110,7 +110,7 @@ let suggest_common env ppid used ids_typ skip =
       S.empty (named_context env)
   in
   let all = S.diff all skip in
-  let fwd_typ = close_fwd env ids_typ in
+  let fwd_typ = close_fwd env (Evd.from_env env) ids_typ in
   if !Flags.debug then begin
     print (str "All "        ++ pr_set false all);
     print (str "Type "       ++ pr_set false ids_typ);
diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli
index dfc233e8fa..93dbd33ae4 100644
--- a/vernac/proof_using.mli
+++ b/vernac/proof_using.mli
@@ -11,7 +11,8 @@
 (** Utility code for section variables handling in Proof using... *)
 
 val process_expr :
-  Environ.env -> Vernacexpr.section_subset_expr -> Constr.types list ->
+  Environ.env -> Evd.evar_map ->
+  Vernacexpr.section_subset_expr -> EConstr.types list ->
     Names.Id.t list
 
 val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit
@@ -24,3 +25,5 @@ val get_default_proof_using : unit -> Vernacexpr.section_subset_expr option
 
 val proof_using_opt_name : string list
 (** For the stm *)
+
+val using_from_string : string -> Vernacexpr.section_subset_expr
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3ced38d6ea..b6e7d22732 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -57,14 +57,16 @@ module DefAttributes = struct
     program : bool;
     deprecated : Deprecation.t option;
     canonical_instance : bool;
+    using : Vernacexpr.section_subset_expr option;
   }
 
   let parse f =
     let open Attributes in
-    let (((locality, deprecated), polymorphic), program), canonical_instance =
-      parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance) f
+    let ((((locality, deprecated), polymorphic), program), canonical_instance), using =
+      parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance ++ using) f
     in
-    { polymorphic; program; locality; deprecated; canonical_instance }
+    let using = Option.map Proof_using.using_from_string using in
+    { polymorphic; program; locality; deprecated; canonical_instance; using }
 end
 
 let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l))
@@ -496,6 +498,25 @@ let program_inference_hook env sigma ev =
     user_err Pp.(str "The statement obligations could not be resolved \
                       automatically, write a statement definition first.")
 
+let vernac_set_used_variables ~pstate e : Declare.Proof.t =
+  let env = Global.env () in
+  let sigma, _ = Declare.Proof.get_current_context pstate in
+  let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in
+  let tys = List.map snd (initial_goals (Declare.Proof.get pstate)) in
+  let l = Proof_using.process_expr env sigma e tys in
+  let vars = Environ.named_context env in
+  List.iter (fun id ->
+    if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then
+      user_err ~hdr:"vernac_set_used_variables"
+        (str "Unknown variable: " ++ Id.print id))
+    l;
+  let _, pstate = Declare.Proof.set_used_variables pstate l 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 =
@@ -525,7 +546,7 @@ let post_check_evd ~udecl ~poly evd =
   else (* We fix the variables to ensure they won't be lowered to Set *)
     Evd.fix_undefined_variables evd
 
-let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
+let start_lemma_com ~program_mode ~poly ~scope ~kind ?using ?hook thms =
   let env0 = Global.env () in
   let flags = Pretyping.{ all_no_fail_flags with program_mode } in
   let decl = fst (List.hd thms) in
@@ -533,17 +554,20 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
   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
-  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
-    let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
-    Declare.Proof.start_with_initialization ~info ~cinfo:thm evd
-  | RecLemmas.Mutual { mutual_info; cinfo ; possible_guards } ->
-    let cinfo = List.map (Declare.CInfo.to_constr evd) cinfo in
-    let evd = post_check_evd ~udecl ~poly evd in
-    let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
-    Declare.Proof.start_mutual_with_initialization ~info ~cinfo evd ~mutual_info (Some possible_guards)
+  let pstate =
+    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
+      let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
+      Declare.Proof.start_with_initialization ~info ~cinfo:thm evd
+    | RecLemmas.Mutual { mutual_info; cinfo ; possible_guards } ->
+      let cinfo = List.map (Declare.CInfo.to_constr evd) cinfo in
+      let evd = post_check_evd ~udecl ~poly evd in
+      let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
+      Declare.Proof.start_mutual_with_initialization ~info ~cinfo evd ~mutual_info (Some possible_guards)
+  in
+  vernac_set_used_variables_opt ?using pstate
 
 let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function
 | Coercion ->
@@ -583,7 +607,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
   let program_mode = atts.program in
   let poly = atts.polymorphic in
   let name = vernac_definition_name lid local in
-  start_lemma_com ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?hook [(name, pl), (bl, t)]
+  start_lemma_com ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?using:atts.using ?hook [(name, pl), (bl, t)]
 
 let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_opt =
   let open DefAttributes in
@@ -604,7 +628,7 @@ let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_
   else
     let () =
       ComDefinition.do_definition ~name:name.v
-        ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook in
+        ~poly:atts.polymorphic ~scope ~kind ?using:atts.using pl bl red_option c typ_opt ?hook in
     pm
 
 (* NB: pstate argument to use combinators easily *)
@@ -613,7 +637,7 @@ let vernac_start_proof ~atts kind l =
   let scope = enforce_locality_exp atts.locality NoDischarge in
   if Dumpglob.dump () then
     List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
-  start_lemma_com ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) l
+  start_lemma_com ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) ?using:atts.using l
 
 let vernac_end_proof ~lemma ~pm = let open Vernacexpr in function
   | Admitted ->
@@ -639,6 +663,8 @@ let vernac_assumption ~atts discharge kind l nl =
           match scope with
             | Global _ -> Dumpglob.dump_definition lid false "ax"
             | Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
+  if Option.has_some atts.using then
+    Attributes.unsupported_attributes  ["using",VernacFlagEmpty];
   ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l
 
 let is_polymorphic_inductive_cumulativity =
@@ -842,16 +868,17 @@ let vernac_fixpoint_interactive ~atts discharge l =
   let scope = vernac_fixpoint_common ~atts discharge l in
   if atts.program then
     CErrors.user_err Pp.(str"Program Fixpoint requires a body");
-  ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic l
+  vernac_set_used_variables_opt ?using:atts.using
+    (ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic l)
 
 let vernac_fixpoint ~atts ~pm discharge l =
   let open DefAttributes in
   let scope = vernac_fixpoint_common ~atts discharge l in
   if atts.program then
     (* XXX: Switch to the attribute system and match on ~atts *)
-    ComProgramFixpoint.do_fixpoint ~pm ~scope ~poly:atts.polymorphic l
+    ComProgramFixpoint.do_fixpoint ~pm ~scope ~poly:atts.polymorphic ?using:atts.using l
   else
-    let () = ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic l in
+    let () = ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic ?using:atts.using l in
     pm
 
 let vernac_cofixpoint_common ~atts discharge l =
@@ -864,15 +891,16 @@ 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");
-  ComFixpoint.do_cofixpoint_interactive ~scope ~poly:atts.polymorphic l
+  vernac_set_used_variables_opt ?using:atts.using
+    (ComFixpoint.do_cofixpoint_interactive ~scope ~poly:atts.polymorphic l)
 
 let vernac_cofixpoint ~atts ~pm discharge l =
   let open DefAttributes in
   let scope = vernac_cofixpoint_common ~atts discharge l in
   if atts.program then
-    ComProgramFixpoint.do_cofixpoint ~pm ~scope ~poly:atts.polymorphic l
+    ComProgramFixpoint.do_cofixpoint ~pm ~scope ~poly:atts.polymorphic ?using:atts.using l
   else
-    let () = ComFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic l in
+    let () = ComFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic ?using:atts.using l in
     pm
 
 let vernac_scheme l =
@@ -1223,21 +1251,6 @@ let vernac_set_end_tac ~pstate tac =
   (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
   Declare.Proof.set_endline_tactic tac pstate
 
-let vernac_set_used_variables ~pstate e : Declare.Proof.t =
-  let env = Global.env () in
-  let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in
-  let tys = List.map snd (initial_goals (Declare.Proof.get pstate)) in
-  let tys = List.map EConstr.Unsafe.to_constr tys in
-  let l = Proof_using.process_expr env e tys in
-  let vars = Environ.named_context env in
-  List.iter (fun id ->
-    if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then
-      user_err ~hdr:"vernac_set_used_variables"
-        (str "Unknown variable: " ++ Id.print id))
-    l;
-  let _, pstate = Declare.Proof.set_used_variables pstate l in
-  pstate
-
 (*****************************)
 (* Auxiliary file management *)
 
-- 
cgit v1.2.3