Merge PR #13393: [proof using] Remove duplicate code, refactor.

Reviewed-by: gares
Ack-by: SkySkimmer

8 files changed, 45 insertions, 44 deletions

diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index b3ffb864f2..2e48313630 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -111,6 +111,10 @@ 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 definition_using env evd ~body ~types ~using =
+  let terms = Option.List.cons types [body] in
+  Option.map (fun using -> Proof_using.definition_using env evd ~using ~terms) using
+
 let do_definition ?hook ~name ~scope ~poly ?typing_flags ~kind ?using udecl bl red_option c ctypopt =
   let program_mode = false in
   let env = Global.env() in
@@ -120,11 +124,7 @@ let do_definition ?hook ~name ~scope ~poly ?typing_flags ~kind ?using udecl bl r
   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 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 ~kind ?hook ~udecl ~poly ?typing_flags () in
@@ -141,11 +141,7 @@ let do_definition_program ?hook ~pm ~name ~scope ~poly ?typing_flags ~kind ?usin
   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 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
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 0cf0b07822..0f817ffbd1 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -259,13 +259,10 @@ let build_recthms ~indexes ?using fixnames fixtypes fiximps =
   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 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 ~using ~terms) using in
         let args = List.map Context.Rel.Declaration.get_name ctx in
         Declare.CInfo.make ~name ~typ ~args ~impargs ?using ()
       ) fixnames fixtypes fiximps
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 3c4a651cf5..0651f3330e 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -259,10 +259,9 @@ let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?typing_flags ?using r
   let evars, _, evars_def, evars_typ =
     RetrieveObl.retrieve_obligations env recname sigma 0 def typ
   in
-  let using = using |> Option.map (fun expr ->
+  let using =
     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))
+    Option.map (fun using -> Proof_using.definition_using env sigma ~using ~terms) using
   in
   let uctx = Evd.evar_universe_context sigma in
   let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ ?using () in
@@ -294,11 +293,8 @@ let do_program_recursive ~pm ~scope ~poly ?typing_flags ?using 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 terms = [def; typ] in
+    let using = Option.map (fun using -> Proof_using.definition_using env evd ~using ~terms) using 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
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 48aa329e5e..607ba18a95 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -57,7 +57,7 @@ module CInfo = struct
     (** Names to pre-introduce  *)
     ; impargs : Impargs.manual_implicits
     (** Explicitily declared implicit arguments  *)
-    ; using : Names.Id.Set.t option
+    ; using : Proof_using.t option
     (** Explicit declaration of section variables used by the constant *)
     }
 
@@ -1478,11 +1478,10 @@ let start_mutual_with_initialization ~info ~cinfo ~mutual_info sigma snl =
 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 =
+let set_used_variables ps ~using =
   let open Context.Named.Declaration in
   let env = Global.env () in
-  let ids = List.fold_right Id.Set.add l Id.Set.empty in
-  let ctx = Environ.keep_hyps env ids in
+  let ctx = Environ.keep_hyps env using in
   let ctx_set =
     List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in
   let vars_of = Environ.global_vars_set in
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 37a61cc4f0..81558e6f6b 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -79,7 +79,7 @@ module CInfo : sig
     -> typ:'constr
     -> ?args:Name.t list
     -> ?impargs:Impargs.manual_implicits
-    -> ?using:Names.Id.Set.t
+    -> ?using:Proof_using.t
     -> unit
     -> 'constr t
 
@@ -244,7 +244,7 @@ module Proof : sig
 
   (** Sets the section variables assumed by the proof, returns its closure
    * (w.r.t. type dependencies and let-ins covered by it) *)
-  val set_used_variables : t -> Names.Id.t list -> Constr.named_context * t
+  val set_used_variables : t -> using:Proof_using.t -> Constr.named_context * t
 
   (** Gets the set of variables declared to be used by the proof. None means
       no "Proof using" or #[using] was given *)
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index d859fcafe2..01e7b7cc3d 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -64,6 +64,12 @@ let process_expr env sigma e ty =
   let s = Id.Set.union v_ty (process_expr env sigma e v_ty) in
   Id.Set.elements s
 
+type t = Names.Id.Set.t
+
+let definition_using env evd ~using ~terms =
+  let l = process_expr env evd using terms in
+  Names.Id.Set.(List.fold_right add l empty)
+
 let name_set id expr = known_names := (id,expr) :: !known_names
 
 let minimize_hyps env ids =
diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli
index 93dbd33ae4..60db4d60e6 100644
--- a/vernac/proof_using.mli
+++ b/vernac/proof_using.mli
@@ -10,10 +10,17 @@
 
 (** Utility code for section variables handling in Proof using... *)
 
-val process_expr :
-  Environ.env -> Evd.evar_map ->
-  Vernacexpr.section_subset_expr -> EConstr.types list ->
-    Names.Id.t list
+(** At some point it would be good to make this abstract *)
+type t = Names.Id.Set.t
+
+(** Process a [using] expression in definitions to provide the list of
+    used terms *)
+val definition_using
+  : Environ.env
+  -> Evd.evar_map
+  -> using:Vernacexpr.section_subset_expr
+  -> terms:EConstr.constr list
+  -> t
 
 val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index c38cfbadc2..38ca836b32 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -563,19 +563,19 @@ 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 vernac_set_used_variables ~pstate using : 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).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 terms = List.map snd (initial_goals (Declare.Proof.get pstate)) in
+  let using = Proof_using.definition_using env sigma ~using ~terms 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
+  Names.Id.Set.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))
+    using;
+  let _, pstate = Declare.Proof.set_used_variables pstate ~using in
   pstate
 
 let vernac_set_used_variables_opt ?using pstate =