diff options
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 4d26c4f533..827747c6b8 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -161,7 +161,7 @@ let save with_clean id const (locality,kind) hook = (locality, ConstRef kn) in if with_clean then Pfedit.delete_current_proof (); - hook l r; + Option.default (fun _ _ -> ()) hook l r; definition_message id |