Merge PR #8447: Cleaning in the retroknowledge

9 files changed, 118 insertions, 95 deletions

diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index ff977416df..31dede6f5d 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -661,11 +661,11 @@ let rec lambda_of_constr env c =
 
     (* translation of the argument *)
     let la = lambda_of_constr env a in
-    let entry = mkInd ind in
+    let gr = GlobRef.IndRef ind in
     let la =
       try
         Retroknowledge.get_vm_before_match_info env.global_env.retroknowledge
-          entry la
+          gr la
       with Not_found -> la
     in
     (* translation of the type *)
@@ -723,7 +723,7 @@ and lambda_of_app env f args =
     (try
       (* We delay the compilation of arguments to avoid an exponential behavior *)
       let f = Retroknowledge.get_vm_compiling_info env.global_env.retroknowledge
-          (mkConstU (kn,u)) in
+          (GlobRef.ConstRef kn) in
       let args = lambda_of_args env 0 args in
       f args
     with Not_found ->
@@ -736,6 +736,7 @@ and lambda_of_app env f args =
   | Construct (c,_) ->
     let tag, nparams, arity = Renv.get_construct_info env c in
     let nargs = Array.length args in
+    let gr = GlobRef.ConstructRef c in
     if Int.equal (nparams + arity) nargs then (* fully applied *)
       (* spiwack: *)
       (* 1/ tries to compile the constructor in an optimal way,
@@ -750,7 +751,7 @@ and lambda_of_app env f args =
         try
           Retroknowledge.get_vm_constant_static_info
             env.global_env.retroknowledge
-            f args
+            gr args
         with NotClosed ->
           (* 2/ if the arguments are not all closed (this is
                               expectingly (and it is currently the case) the only
@@ -771,7 +772,7 @@ and lambda_of_app env f args =
           let args = lambda_of_args env nparams rargs in
           Retroknowledge.get_vm_constant_dynamic_info
             env.global_env.retroknowledge
-            f args
+            gr args
       with Not_found ->
         (* 3/ if no special behavior is available, then the compiler
            falls back to the normal behavior *)
@@ -784,7 +785,7 @@ and lambda_of_app env f args =
       (try
          (Retroknowledge.get_vm_constant_dynamic_info
             env.global_env.retroknowledge
-            f) args
+            gr) args
        with Not_found ->
          if nparams <= nargs then (* got all parameters *)
            makeblock tag 0 arity args
diff --git a/kernel/environ.ml b/kernel/environ.ml
index e7efa5e2c9..62c14f6f07 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -693,12 +693,12 @@ let register_one env field entry =
   { env with retroknowledge = Retroknowledge.add_field env.retroknowledge field entry }
 
 (* [register env field entry] may register several fields when needed *)
-let register env field entry =
+let register env field gr =
   match field with
-    | KInt31 (grp, Int31Type) ->
-        let i31c = match kind entry with
-                     | Ind i31t -> mkConstructUi (i31t, 1)
-		     | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.")
-	in
-        register_one (register_one env (KInt31 (grp,Int31Constructor)) i31c) field entry
-    | field -> register_one env field entry
+  | KInt31 Int31Type ->
+    let i31c = match gr with
+      | GlobRef.IndRef i31t -> GlobRef.ConstructRef (i31t, 1)
+      | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.")
+    in
+    register_one (register_one env (KInt31 Int31Constructor) i31c) field gr
+  | field -> register_one env field gr
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f45b7be821..1343b9029b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -325,7 +325,7 @@ val retroknowledge : (retroknowledge->'a) -> env -> 'a
 
 val registered : env -> field -> bool
 
-val register : env -> field -> Retroknowledge.entry -> env
+val register : env -> field -> GlobRef.t -> env
 
 (** Native compiler *)
 val no_link_info : link_info
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 98a9973117..9435f46c6b 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -267,7 +267,7 @@ let subst_structure subst = subst_structure subst do_delta_codom
 (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *)
 let add_retroknowledge =
   let perform rkaction env = match rkaction with
-    | Retroknowledge.RKRegister (f, e) when (isConst e || isInd e) ->
+    | Retroknowledge.RKRegister (f, ((GlobRef.ConstRef _ | GlobRef.IndRef _) as e)) ->
       Environ.register env f e
     | _ ->
       CErrors.anomaly ~label:"Modops.add_retroknowledge"
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 122fe95df4..ab40c643f9 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -373,14 +373,14 @@ let is_lazy env prefix t =
   | App (f,args) ->
      begin match kind f with
      | Construct (c,_) ->
-	let entry = mkInd (fst c) in
-	(try
-	    let _ =
-              Retroknowledge.get_native_before_match_info env.retroknowledge
-							  entry prefix c Llazy;
-	    in
+       let gr = GlobRef.IndRef (fst c) in
+       (try
+          let _ =
+            Retroknowledge.get_native_before_match_info env.retroknowledge
+              gr prefix c Llazy;
+          in
 	    false
-	  with Not_found -> true)
+        with Not_found -> true)
      | _ -> true
      end
   | LetIn _ | Case _ | Proj _ -> true
@@ -482,12 +482,12 @@ let rec lambda_of_constr cache env sigma c =
       in
       (* translation of the argument *)
       let la = lambda_of_constr cache env sigma a in
-      let entry = mkInd ind in
+      let gr = GlobRef.IndRef ind in
       let la =
-	try
-          Retroknowledge.get_native_before_match_info (env).retroknowledge
-						      entry prefix (ind,1) la
-	with Not_found -> la
+        try
+         Retroknowledge.get_native_before_match_info (env).retroknowledge
+           gr prefix (ind,1) la
+        with Not_found -> la
       in
       (* translation of the type *)
       let lt = lambda_of_constr cache env sigma t in
@@ -536,7 +536,7 @@ and lambda_of_app cache env sigma f args =
           let prefix = get_const_prefix env kn in
 	  (* We delay the compilation of arguments to avoid an exponential behavior *)
 	  let f = Retroknowledge.get_native_compiling_info
-                    (env).retroknowledge (mkConst kn) prefix in
+                    (env).retroknowledge (GlobRef.ConstRef kn) prefix in
           let args = lambda_of_args cache env sigma 0 args in
 	  f args
       with Not_found ->
@@ -561,17 +561,18 @@ and lambda_of_app cache env sigma f args =
       let expected = nparams + arity in
       let nargs = Array.length args in
       let prefix = get_mind_prefix env (fst (fst c)) in
+      let gr = GlobRef.ConstructRef c in
       if Int.equal nargs expected then 
       try
 	try
 	  Retroknowledge.get_native_constant_static_info
                          (env).retroknowledge
-                         f args
+                         gr args
           with NotClosed ->
 	    assert (Int.equal nparams 0); (* should be fine for int31 *)
             let args = lambda_of_args cache env sigma nparams args in
 	    Retroknowledge.get_native_constant_dynamic_info
-                           (env).retroknowledge f prefix c args
+                           (env).retroknowledge gr prefix c args
         with Not_found ->
           let args = lambda_of_args cache env sigma nparams args in
           makeblock env c u tag args
@@ -579,7 +580,7 @@ and lambda_of_app cache env sigma f args =
         let args = lambda_of_args cache env sigma 0 args in
 	(try
 	    Retroknowledge.get_native_constant_dynamic_info
-              (env).retroknowledge f prefix c args
+              (env).retroknowledge gr prefix c args
 	  with Not_found ->
             mkLapp (Lconstruct (prefix, (c,u))) args)
   | _ -> 
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 34f62defb8..e51c25c06b 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -19,12 +19,9 @@ open Names
 open Constr
 
 (* The retroknowledge defines a bijective correspondance between some
-   [entry]-s (which are, in fact, merely terms) and [field]-s which
+   [entry]-s (which are, in fact, merely names) and [field]-s which
    are roles assigned to these entries. *)
 
-(* aliased type for clarity purpose*)
-type entry = Constr.t
-
 type int31_field =
   | Int31Bits
   | Int31Type
@@ -53,8 +50,37 @@ type int31_field =
   | Int31Lxor
 
 type field =
-  | KInt31 of string*int31_field
-
+  | KInt31 of int31_field
+
+let int31_field_of_string =
+  function
+  | "bits" -> Int31Bits
+  | "type" -> Int31Type
+  | "twice" -> Int31Twice
+  | "twice_plus_one" -> Int31TwicePlusOne
+  | "phi" -> Int31Phi
+  | "phi_inv" -> Int31PhiInv
+  | "plus" -> Int31Plus
+  | "plusc" -> Int31PlusC
+  | "pluscarryc" -> Int31PlusCarryC
+  | "minus" -> Int31Minus
+  | "minusc" -> Int31MinusC
+  | "minuscarryc" -> Int31MinusCarryC
+  | "times" -> Int31Times
+  | "timesc" -> Int31TimesC
+  | "div21" -> Int31Div21
+  | "div" -> Int31Div
+  | "diveucl" -> Int31Diveucl
+  | "addmuldiv" -> Int31AddMulDiv
+  | "compare" -> Int31Compare
+  | "head0" -> Int31Head0
+  | "tail0" -> Int31Tail0
+  | "lor" -> Int31Lor
+  | "land" -> Int31Land
+  | "lxor" -> Int31Lxor
+  | s -> CErrors.user_err Pp.(str "Registering unknown int31 operator " ++ str s)
+
+let int31_path = DirPath.make [ Id.of_string "int31" ]
 
 (* record representing all the flags of the internal state of the kernel *)
 type flags = {fastcomputation : bool}
@@ -68,19 +94,13 @@ type flags = {fastcomputation : bool}
 module Proactive =
   Map.Make (struct type t = field let compare = Pervasives.compare end)
 
-type proactive = entry Proactive.t
+type proactive = GlobRef.t Proactive.t
 
 (* The [reactive] knowledge contains the mapping
    [entry->field]. Fields are later to be interpreted as a
    [reactive_info]. *)
 
-module EntryOrd =
-struct
-  type t = entry
-  let compare = Constr.compare
-end
-
-module Reactive = Map.Make (EntryOrd)
+module Reactive = GlobRef.Map
 
 type reactive_info = {(*information required by the compiler of the VM *)
   vm_compiling :
@@ -127,7 +147,7 @@ and retroknowledge = {flags : flags; proactive : proactive; reactive : reactive}
 (* As per now, there is only the possibility of registering things
    the possibility of unregistering or changing the flag is under study *)
 type action =
-    | RKRegister of field*entry
+    | RKRegister of field * GlobRef.t
 
 
 (*initialisation*)
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 02d961d893..0a2ef5300e 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -13,9 +13,6 @@ open Constr
 
 type retroknowledge
 
-(** aliased type for clarity purpose*)
-type entry = Constr.t
-
 (** the following types correspond to the different "things"
    the kernel can learn about.*)
 type int31_field =
@@ -46,14 +43,18 @@ type int31_field =
   | Int31Lxor
 
 type field =
-  | KInt31 of string*int31_field
+  | KInt31 of int31_field
+
+val int31_field_of_string : string -> int31_field
+
+val int31_path : DirPath.t
 
 (** This type represent an atomic action of the retroknowledge. It
    is stored in the compiled libraries 
    As per now, there is only the possibility of registering things
    the possibility of unregistering or changing the flag is under study *)
 type action =
-    | RKRegister of field*entry
+    | RKRegister of field * GlobRef.t
 
 
 (** initial value for retroknowledge *)
@@ -64,7 +65,7 @@ val initial_retroknowledge : retroknowledge
    and the continuation cont of the bytecode compilation
    returns the compilation of id in cont if it has a specific treatment
    or raises Not_found if id should be compiled as usual *)
-val get_vm_compiling_info  : retroknowledge -> entry ->
+val get_vm_compiling_info  : retroknowledge -> GlobRef.t ->
                              Cinstr.lambda array -> Cinstr.lambda
 (*Given an identifier id (usually Construct _)
    and its argument array, returns a function that tries an ad-hoc optimisated
@@ -73,7 +74,7 @@ val get_vm_compiling_info  : retroknowledge -> entry ->
    raises Not_found if id should be compiled as usual, and expectingly
    CBytecodes.NotClosed if the term is not a closed constructor pattern
    (a constant for the compiler) *)
-val get_vm_constant_static_info : retroknowledge -> entry ->
+val get_vm_constant_static_info : retroknowledge -> GlobRef.t ->
                                    constr array -> Cinstr.lambda
 
 (*Given an identifier id (usually Construct _ )
@@ -81,45 +82,45 @@ val get_vm_constant_static_info : retroknowledge -> entry ->
    of id+args+cont when id has a specific treatment (in the case of
    31-bit integers, that would be the dynamic compilation into integers)
    or raises Not_found if id should be compiled as usual *)
-val get_vm_constant_dynamic_info : retroknowledge -> entry ->
+val get_vm_constant_dynamic_info : retroknowledge -> GlobRef.t ->
                                    Cinstr.lambda array -> Cinstr.lambda
 
 (** Given a type identifier, this function is used before compiling a match
    over this type. In the case of 31-bit integers for instance, it is used
    to add the instruction sequence which would perform a dynamic decompilation
    in case the argument of the match is not in coq representation *)
-val get_vm_before_match_info : retroknowledge -> entry -> Cinstr.lambda
+val get_vm_before_match_info : retroknowledge -> GlobRef.t -> Cinstr.lambda
                                                        -> Cinstr.lambda
 
 (** Given a type identifier, this function is used by pretyping/vnorm.ml to
    recover the elements of that type from their compiled form if it's non
    standard (it is used (and can be used) only when the compiled form
    is not a block *)
-val get_vm_decompile_constant_info : retroknowledge -> entry -> int -> constr
+val get_vm_decompile_constant_info : retroknowledge -> GlobRef.t -> int -> constr
 
 
-val get_native_compiling_info  : retroknowledge -> entry -> Nativeinstr.prefix ->
+val get_native_compiling_info  : retroknowledge -> GlobRef.t -> Nativeinstr.prefix ->
 				 Nativeinstr.lambda array -> Nativeinstr.lambda
 
-val get_native_constant_static_info : retroknowledge -> entry ->
+val get_native_constant_static_info : retroknowledge -> GlobRef.t ->
                                       constr array -> Nativeinstr.lambda
 
-val get_native_constant_dynamic_info : retroknowledge -> entry ->
+val get_native_constant_dynamic_info : retroknowledge -> GlobRef.t ->
                                        Nativeinstr.prefix -> constructor ->
 				       Nativeinstr.lambda array ->
 				       Nativeinstr.lambda
 
-val get_native_before_match_info : retroknowledge -> entry ->
+val get_native_before_match_info : retroknowledge -> GlobRef.t ->
 				   Nativeinstr.prefix -> constructor ->
 				   Nativeinstr.lambda -> Nativeinstr.lambda
 
 
 (** the following functions are solely used in Environ and Safe_typing to implement
    the functions  register and unregister (and mem) of Environ *)
-val add_field : retroknowledge -> field -> entry -> retroknowledge
+val add_field : retroknowledge -> field -> GlobRef.t -> retroknowledge
 val mem : retroknowledge -> field -> bool
 (* val remove : retroknowledge -> field -> retroknowledge *)
-val find : retroknowledge -> field -> entry
+val find : retroknowledge -> field -> GlobRef.t
 
 
 (** Dispatching type for the above [get_*] functions. *)
@@ -161,4 +162,4 @@ val empty_reactive_info : reactive_info
 
 (** Hook to be set after the compiler are installed to dispatch fields
     into the above [get_*] functions. *)
-val dispatch_hook : (retroknowledge -> entry -> field -> reactive_info) Hook.t
+val dispatch_hook : (retroknowledge -> GlobRef.t -> field -> reactive_info) Hook.t
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 6c87ff570f..9d302c69fb 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -892,8 +892,8 @@ let retroknowledge f senv =
   Environ.retroknowledge f (env_of_senv senv)
 [@@@ocaml.warning "+3"]
 
-let register field value by_clause senv =
-  (* todo : value closed, by_clause safe, by_clause of the proper type*)
+let register field value senv =
+  (* todo : value closed *)
   (* spiwack : updates the safe_env with the information that the register
      action has to be performed (again) when the environment is imported *)
   { senv with
@@ -977,39 +977,39 @@ let dispatch =
      it to the name of the coq definition in the reactive retroknowledge) *)
   let int31_op n op prim kn =
     { empty_reactive_info with
-      vm_compiling = Some (Clambda.compile_prim n op kn);
-      native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn));
+      vm_compiling = Some (Clambda.compile_prim n op (kn, Univ.Instance.empty)); (*XXX: FIXME universes? *)
+      native_compiling = Some (Nativelambda.compile_prim prim kn);
     }
   in
 
 fun rk value field ->
   (* subfunction which shortens the (very common) dispatch of operations *)
   let int31_op_from_const n op prim =
-    match Constr.kind value with
-      | Constr.Const kn ->  int31_op n op prim kn
+    match value with
+      | GlobRef.ConstRef kn -> int31_op n op prim kn
       | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant.")
   in
   let int31_binop_from_const op prim = int31_op_from_const 2 op prim in
   let int31_unop_from_const op prim = int31_op_from_const 1 op prim in
   match field with
-    | KInt31 (grp, Int31Type) ->
+    | KInt31 Int31Type ->
         let int31bit =
           (* invariant : the type of bits is registered, otherwise the function
              would raise Not_found. The invariant is enforced in safe_typing.ml *)
           match field with
-          | KInt31 (grp, Int31Type) -> Retroknowledge.find rk (KInt31 (grp,Int31Bits))
+          | KInt31 Int31Type -> Retroknowledge.find rk (KInt31 Int31Bits)
           | _ -> anomaly ~label:"Environ.register"
               (Pp.str "add_int31_decompilation_from_type called with an abnormal field.")
         in
         let i31bit_type =
-          match Constr.kind int31bit with
-          | Constr.Ind (i31bit_type,_) -> i31bit_type
+          match int31bit with
+          | GlobRef.IndRef i31bit_type -> i31bit_type
           |  _ -> anomaly ~label:"Environ.register"
               (Pp.str "Int31Bits should be an inductive type.")
         in
         let int31_decompilation =
-          match Constr.kind value with
-          | Constr.Ind (i31t,_) ->
+          match value with
+          | GlobRef.IndRef i31t ->
               constr_of_int31 i31t i31bit_type
           | _ -> anomaly ~label:"Environ.register"
               (Pp.str "should be an inductive type.")
@@ -1019,46 +1019,46 @@ fun rk value field ->
           vm_before_match = Some Clambda.int31_escape_before_match;
           native_before_match = Some (Nativelambda.before_match_int31 i31bit_type);
         }
-    | KInt31 (_, Int31Constructor) ->
+    | KInt31 Int31Constructor ->
         { empty_reactive_info with
           vm_constant_static = Some Clambda.compile_structured_int31;
           vm_constant_dynamic = Some Clambda.dynamic_int31_compilation;
           native_constant_static = Some Nativelambda.compile_static_int31;
           native_constant_dynamic = Some Nativelambda.compile_dynamic_int31;
         }
-    | KInt31 (_, Int31Plus) -> int31_binop_from_const Cbytecodes.Kaddint31
+    | KInt31 Int31Plus -> int31_binop_from_const Cbytecodes.Kaddint31
                                                           CPrimitives.Int31add
-    | KInt31 (_, Int31PlusC) -> int31_binop_from_const Cbytecodes.Kaddcint31
+    | KInt31 Int31PlusC -> int31_binop_from_const Cbytecodes.Kaddcint31
                                                            CPrimitives.Int31addc
-    | KInt31 (_, Int31PlusCarryC) -> int31_binop_from_const Cbytecodes.Kaddcarrycint31
+    | KInt31 Int31PlusCarryC -> int31_binop_from_const Cbytecodes.Kaddcarrycint31
                                                                 CPrimitives.Int31addcarryc
-    | KInt31 (_, Int31Minus) -> int31_binop_from_const Cbytecodes.Ksubint31
+    | KInt31 Int31Minus -> int31_binop_from_const Cbytecodes.Ksubint31
                                                            CPrimitives.Int31sub
-    | KInt31 (_, Int31MinusC) -> int31_binop_from_const Cbytecodes.Ksubcint31
+    | KInt31 Int31MinusC -> int31_binop_from_const Cbytecodes.Ksubcint31
                                                             CPrimitives.Int31subc
-    | KInt31 (_, Int31MinusCarryC) -> int31_binop_from_const
+    | KInt31 Int31MinusCarryC -> int31_binop_from_const
                                         Cbytecodes.Ksubcarrycint31 CPrimitives.Int31subcarryc
-    | KInt31 (_, Int31Times) -> int31_binop_from_const Cbytecodes.Kmulint31
+    | KInt31 Int31Times -> int31_binop_from_const Cbytecodes.Kmulint31
                                                            CPrimitives.Int31mul
-    | KInt31 (_, Int31TimesC) -> int31_binop_from_const Cbytecodes.Kmulcint31
+    | KInt31 Int31TimesC -> int31_binop_from_const Cbytecodes.Kmulcint31
                                                            CPrimitives.Int31mulc
-    | KInt31 (_, Int31Div21) -> int31_op_from_const 3 Cbytecodes.Kdiv21int31
+    | KInt31 Int31Div21 -> int31_op_from_const 3 Cbytecodes.Kdiv21int31
                                                            CPrimitives.Int31div21
-    | KInt31 (_, Int31Diveucl) -> int31_binop_from_const Cbytecodes.Kdivint31
+    | KInt31 Int31Diveucl -> int31_binop_from_const Cbytecodes.Kdivint31
                                                          CPrimitives.Int31diveucl
-    | KInt31 (_, Int31AddMulDiv) -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31
+    | KInt31 Int31AddMulDiv -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31
                                                          CPrimitives.Int31addmuldiv
-    | KInt31 (_, Int31Compare) -> int31_binop_from_const Cbytecodes.Kcompareint31
+    | KInt31 Int31Compare -> int31_binop_from_const Cbytecodes.Kcompareint31
                                                              CPrimitives.Int31compare
-    | KInt31 (_, Int31Head0) -> int31_unop_from_const Cbytecodes.Khead0int31
+    | KInt31 Int31Head0 -> int31_unop_from_const Cbytecodes.Khead0int31
                                                           CPrimitives.Int31head0
-    | KInt31 (_, Int31Tail0) -> int31_unop_from_const Cbytecodes.Ktail0int31
+    | KInt31 Int31Tail0 -> int31_unop_from_const Cbytecodes.Ktail0int31
                                                           CPrimitives.Int31tail0
-    | KInt31 (_, Int31Lor) -> int31_binop_from_const Cbytecodes.Klorint31
+    | KInt31 Int31Lor -> int31_binop_from_const Cbytecodes.Klorint31
                                                          CPrimitives.Int31lor
-    | KInt31 (_, Int31Land) -> int31_binop_from_const Cbytecodes.Klandint31
+    | KInt31 Int31Land -> int31_binop_from_const Cbytecodes.Klandint31
                                                           CPrimitives.Int31land
-    | KInt31 (_, Int31Lxor) -> int31_binop_from_const Cbytecodes.Klxorint31
+    | KInt31 Int31Lxor -> int31_binop_from_const Cbytecodes.Klxorint31
                                                           CPrimitives.Int31lxor
     | _ -> empty_reactive_info
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 502e2970a1..08b97b718e 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -215,7 +215,7 @@ val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a
 [@@ocaml.deprecated "Use the projection of Environ.env"]
 
 val register :
-  field -> Retroknowledge.entry -> Constr.constr -> safe_transformer0
+  field -> GlobRef.t -> safe_transformer0
 
 val register_inline : Constant.t -> safe_transformer0