From c81254903e1e50a2305cd48ccfb673d9737afc48 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 8 Aug 2013 18:52:52 +0000
Subject: get rid of closures in global/proof state

In some cases, an 'a -> 'b field is changed into an ('a -> b') option
field so that one can forget the closures and marshal the resulting
state

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16683 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/indfun_common.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

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