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
---
 toplevel/command.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'toplevel/command.mli')

diff --git a/toplevel/command.mli b/toplevel/command.mli
index 76a3c58027..fe6a0a4003 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -35,7 +35,8 @@ val interp_definition :
   constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits
 
 val declare_definition : Id.t -> definition_kind ->
-  definition_entry -> Impargs.manual_implicits -> 'a declaration_hook -> 'a
+  definition_entry -> Impargs.manual_implicits ->
+    Globnames.global_reference declaration_hook -> Globnames.global_reference
 
 val do_definition : Id.t -> definition_kind ->
   local_binder list -> red_expr option -> constr_expr ->
-- 
cgit v1.2.3