[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.

1 files changed, 4 insertions, 7 deletions

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