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/indfun.ml | 1 -
 1 file changed, 1 deletion(-)

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

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