From d866ed978ece3b80364dfcf67ee801a556462f29 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 16 Nov 2020 04:05:49 +0100
Subject: [proof using] Remove duplicate code, refactor.

PR #13183 introduced quite a bit of duplicate code, we refactor it and
expose less internals on the way. That should make the API more
robust.
---
 vernac/proof_using.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'vernac/proof_using.ml')

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 =
-- 
cgit v1.2.3