4 files changed, 8 insertions, 8 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 171d51800e..8d5c2fb687 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -70,6 +70,7 @@ type goal_kind = locality * polymorphic * goal_object_kind
 (** Kinds used in library *)
 
 type logical_kind =
+  | IsPrimitive
   | IsAssumption of assumption_object_kind
   | IsDefinition of definition_object_kind
   | IsProof of theorem_kind
diff --git a/library/global.ml b/library/global.ml
index 84d2a37170..784a02449c 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -175,11 +175,8 @@ let with_global f =
   let (a, ctx) = f (env ()) (current_dirpath ()) in
     push_context_set false ctx; a
 
-(* spiwack: register/unregister functions for retroknowledge *)
-let register field value =
-  globalize0 (Safe_typing.register field value)
-
 let register_inline c = globalize0 (Safe_typing.register_inline c)
+let register_inductive c r = globalize0 (Safe_typing.register_inductive c r)
 
 let set_strategy k l =
   globalize0 (Safe_typing.set_strategy k l)
diff --git a/library/global.mli b/library/global.mli
index 40962e21af..df18625a5f 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -142,10 +142,8 @@ val universes_of_global : GlobRef.t -> Univ.AUContext.t
 
 (** {6 Retroknowledge } *)
 
-val register :
-  Retroknowledge.field -> GlobRef.t -> unit
-
 val register_inline : Constant.t -> unit
+val register_inductive : inductive -> CPrimitives.prim_ind -> unit
 
 (** {6 Oracle } *)
 
diff --git a/library/keys.ml b/library/keys.ml
index 58883ccc88..45b6fae2f0 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -25,13 +25,14 @@ type key =
   | KFix
   | KCoFix
   | KRel
+  | KInt
 
 module KeyOrdered = struct
   type t = key
 
   let hash gr =
     match gr with
-    | KGlob gr -> 8 + GlobRef.Ordered.hash gr
+    | KGlob gr -> 9 + GlobRef.Ordered.hash gr
     | KLam -> 0
     | KLet -> 1
     | KProd -> 2
@@ -40,6 +41,7 @@ module KeyOrdered = struct
     | KFix -> 5
     | KCoFix -> 6
     | KRel -> 7
+    | KInt -> 8
 
   let compare gr1 gr2 =
     match gr1, gr2 with
@@ -133,6 +135,7 @@ let constr_key kind c =
       | Evar _ -> raise Not_found
       | Sort _ -> KSort 
       | LetIn _ -> KLet
+      | Int _ -> KInt
     in Some (aux c)
   with Not_found -> None
 
@@ -148,6 +151,7 @@ let pr_key pr_global = function
   | KFix -> str"Fix"
   | KCoFix -> str"CoFix"
   | KRel -> str"Rel"
+  | KInt -> str"Int"
 
 let pr_keyset pr_global v = 
   prlist_with_sep spc (pr_key pr_global) (Keyset.elements v)