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.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 8cccb0bed..5d9c226b7 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -166,7 +166,7 @@ let save with_clean id const (locality,_,kind) hook =
let cook_proof _ =
- let (id,(entry,strength)) = Pfedit.cook_proof () in
+ let (id,(entry,_,strength)) = Pfedit.cook_proof () in
(id,(entry,strength))
let get_proof_clean do_reduce =