diff options
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 4 |
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 |