aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/indfun_common.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/indfun_common.ml')
-rw-r--r--plugins/funind/indfun_common.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 604d7d853..5c37dcec3 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -166,8 +166,8 @@ let save with_clean id const (locality,kind) hook =
let cook_proof _ =
- let (id,(entry,strength,hook)) = Pfedit.cook_proof (fun _ -> ()) in
- (id,(entry,strength,hook))
+ let (id,(entry,strength)) = Pfedit.cook_proof () in
+ (id,(entry,strength))
let get_proof_clean do_reduce =
let result = cook_proof do_reduce in