[funind] Remove unneeded callback.

4 files changed, 11 insertions, 12 deletions

diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index b4f6f92f9c..7cadd4396d 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -33,8 +33,10 @@ val generate_functional_principle :
 
 exception No_graph_found
 
-val make_scheme :   Evd.evar_map ref ->
- (pconstant*Sorts.family) list -> Evd.side_effects Proof_global.proof_entry list
+val make_scheme
+  :  Evd.evar_map ref
+  -> (pconstant*Sorts.family) list
+  -> Evd.side_effects Proof_global.proof_entry list
 
 val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list ->  unit
 val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family)  ->  unit
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 99efe3e5e2..6e19ef4804 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -285,7 +285,6 @@ let derive_inversion fix_names =
           (evd',[])
       in
       Invfun.derive_correctness
-        Functional_principles_types.make_scheme
         fix_names_as_constant
         lind;
       with e when CErrors.noncritical e ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d4cc31c0af..f6b5a06cac 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -736,11 +736,9 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti
 
 (* [derive_correctness make_scheme funs graphs] create correctness and completeness
    lemmas for each function in [funs] w.r.t. [graphs]
-
-   [make_scheme] is Functional_principle_types.make_scheme (dependency pb) and
 *)
 
-let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list) =
+let derive_correctness (funs: pconstant list) (graphs:inductive list) =
   assert (funs <> []);
   assert (graphs <> []);
   let funs = Array.of_list funs and graphs = Array.of_list graphs in
@@ -786,7 +784,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
                (fun entry ->
                   (EConstr.of_constr (fst (fst(Future.force entry.Proof_global.proof_entry_body))), EConstr.of_constr (Option.get entry.Proof_global.proof_entry_type ))
                )
-               (make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs))
+               (Functional_principles_types.make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs))
             )
         )
     in
diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli
index 96601785b6..c7538fae9a 100644
--- a/plugins/funind/invfun.mli
+++ b/plugins/funind/invfun.mli
@@ -12,8 +12,8 @@ val invfun :
   Tactypes.quantified_hypothesis ->
   Names.GlobRef.t option ->
   Evar.t Evd.sigma -> Evar.t list Evd.sigma
-val derive_correctness :
-  (Evd.evar_map ref ->
-   (Constr.pconstant * Sorts.family) list ->
-   'a Proof_global.proof_entry list) ->
-   Constr.pconstant list -> Names.inductive list -> unit
+
+val derive_correctness
+  :  Constr.pconstant list
+  -> Names.inductive list
+  -> unit