From 19b92fb6767b0f9c84ea7d6331d764269734a883 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 15 Jul 2019 15:27:53 +0200
Subject: [funind] Remove unneeded callback.

---
 plugins/funind/invfun.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'plugins/funind/invfun.ml')

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