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

Reviewed-by: gares
Ack-by: SkySkimmer

1 files changed, 6 insertions, 0 deletions

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 =