From e2f27dfcb21c42b72cf8d6a1363251f4c48789cb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 5 Mar 2014 12:06:17 +0100
Subject: Changing Retrokwnoledge entry type from kind_of_term to constr. It
 seems it had no particular purpose.

---
 library/global.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/global.ml b/library/global.ml
index f75c8e5927..9f683b2ff1 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -156,7 +156,7 @@ let type_of_global t = type_of_reference (env ()) t
 
 (* spiwack: register/unregister functions for retroknowledge *)
 let register field value by_clause =
-  globalize0 (Safe_typing.register field (kind_of_term value) by_clause)
+  globalize0 (Safe_typing.register field value by_clause)
 
 let register_inline c = globalize0 (Safe_typing.register_inline c)
 
-- 
cgit v1.2.3