Merge PR #8447: Cleaning in the retroknowledge

21 files changed, 167 insertions, 224 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
 
diff --git a/library/global.ml b/library/global.ml
index e833f71142..5872126a12 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -271,8 +271,8 @@ let with_global f =
     push_context_set false ctx; a
 
 (* spiwack: register/unregister functions for retroknowledge *)
-let register field value by_clause =
-  globalize0 (Safe_typing.register field value by_clause)
+let register field value =
+  globalize0 (Safe_typing.register field value)
 
 let register_inline c = globalize0 (Safe_typing.register_inline c)
 
diff --git a/library/global.mli b/library/global.mli
index 2819c187ed..6aeae9fd02 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -148,7 +148,7 @@ val universes_of_global : GlobRef.t -> Univ.AUContext.t
 (** {6 Retroknowledge } *)
 
 val register :
-  Retroknowledge.field -> Constr.constr -> Constr.constr -> unit
+  Retroknowledge.field -> GlobRef.t -> unit
 
 val register_inline : Constant.t -> unit
 
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 38600695dc..f4555509cc 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -311,78 +311,3 @@ let pr_lpar_id_colon _ _ _ _ = mt ()
 ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY pr_lpar_id_colon
 | [ local_test_lpar_id_colon(x) ] -> [ () ]
 END
-
-(* spiwack: the print functions are incomplete, but I don't know what they are
-	used for *)
-let pr_r_int31_field i31f =
-  str "int31 " ++
-  match i31f with
-    | Retroknowledge.Int31Bits -> str "bits"
-    | Retroknowledge.Int31Type -> str "type"
-    | Retroknowledge.Int31Twice -> str "twice"
-    | Retroknowledge.Int31TwicePlusOne -> str "twice plus one"
-    | Retroknowledge.Int31Phi -> str "phi"
-    | Retroknowledge.Int31PhiInv -> str "phi inv"
-    | Retroknowledge.Int31Plus -> str "plus"
-    | Retroknowledge.Int31Times -> str "times"
-    | Retroknowledge.Int31Constructor -> assert false
-    | Retroknowledge.Int31PlusC -> str "plusc"
-    | Retroknowledge.Int31PlusCarryC -> str "pluscarryc"
-    | Retroknowledge.Int31Minus -> str "minus"
-    | Retroknowledge.Int31MinusC -> str "minusc"
-    | Retroknowledge.Int31MinusCarryC -> str "minuscarryc"
-    | Retroknowledge.Int31TimesC -> str "timesc"
-    | Retroknowledge.Int31Div21 -> str "div21"
-    | Retroknowledge.Int31Div -> str "div"
-    | Retroknowledge.Int31Diveucl -> str "diveucl"
-    | Retroknowledge.Int31AddMulDiv -> str "addmuldiv"
-    | Retroknowledge.Int31Compare -> str "compare"
-    | Retroknowledge.Int31Head0 -> str "head0"
-    | Retroknowledge.Int31Tail0 -> str "tail0"
-    | Retroknowledge.Int31Lor -> str "lor"
-    | Retroknowledge.Int31Land -> str "land"
-    | Retroknowledge.Int31Lxor -> str "lxor"
-
-let pr_retroknowledge_field f =
-  match f with
- (* | Retroknowledge.KEq -> str "equality"
-  | Retroknowledge.KNat natf -> pr_r_nat_field () () () natf
-  | Retroknowledge.KN nf -> pr_r_n_field () () () nf *)
-  | Retroknowledge.KInt31 (group, i31f) -> (pr_r_int31_field i31f) ++
-                                           spc () ++ str "in " ++ qs group
-
-VERNAC ARGUMENT EXTEND retroknowledge_int31
-PRINTED BY pr_r_int31_field
-| [ "int31" "bits" ] -> [ Retroknowledge.Int31Bits ]
-| [ "int31" "type" ] -> [ Retroknowledge.Int31Type ]
-| [ "int31" "twice" ] -> [ Retroknowledge.Int31Twice ]
-| [ "int31" "twice" "plus" "one" ] -> [ Retroknowledge.Int31TwicePlusOne ]
-| [ "int31" "phi" ] -> [ Retroknowledge.Int31Phi ]
-| [ "int31" "phi" "inv" ] -> [ Retroknowledge.Int31PhiInv ]
-| [ "int31" "plus" ] -> [ Retroknowledge.Int31Plus ]
-| [ "int31" "plusc" ] -> [ Retroknowledge.Int31PlusC ]
-| [ "int31" "pluscarryc" ] -> [ Retroknowledge.Int31PlusCarryC ]
-| [ "int31" "minus" ] -> [ Retroknowledge.Int31Minus ]
-| [ "int31" "minusc" ] -> [ Retroknowledge.Int31MinusC ]
-| [ "int31" "minuscarryc" ] -> [ Retroknowledge.Int31MinusCarryC ]
-| [ "int31" "times" ] -> [ Retroknowledge.Int31Times ]
-| [ "int31" "timesc" ] -> [ Retroknowledge.Int31TimesC ]
-| [ "int31" "div21" ] -> [ Retroknowledge.Int31Div21 ]
-| [ "int31" "div" ] -> [ Retroknowledge.Int31Div ]
-| [ "int31" "diveucl" ] -> [ Retroknowledge.Int31Diveucl ]
-| [ "int31" "addmuldiv" ] -> [ Retroknowledge.Int31AddMulDiv ]
-| [ "int31" "compare" ] -> [ Retroknowledge.Int31Compare ]
-| [ "int31" "head0" ] -> [ Retroknowledge.Int31Head0 ]
-| [ "int31" "tail0" ] -> [ Retroknowledge.Int31Tail0 ]
-| [ "int31" "lor" ] -> [ Retroknowledge.Int31Lor ]
-| [ "int31" "land" ] -> [ Retroknowledge.Int31Land ]
-| [ "int31" "lxor" ] -> [ Retroknowledge.Int31Lxor ]
-END
-
-VERNAC ARGUMENT EXTEND retroknowledge_field
-PRINTED BY pr_retroknowledge_field
-(*| [ "equality" ] -> [ Retroknowledge.KEq ]
-| [ retroknowledge_nat(n)] -> [ Retroknowledge.KNat n ]
-| [ retroknowledge_binary_n (n)] -> [ Retroknowledge.KN n ]*)
-| [ retroknowledge_int31 (i) "in" string(g)] -> [ Retroknowledge.KInt31(g,i) ]
-END
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index e477b12cd3..fa70235975 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -72,11 +72,6 @@ val test_lpar_id_colon : unit Pcoq.Entry.t
 
 val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type
 
-(** Spiwack: Primitive for retroknowledge registration *)
-
-val retroknowledge_field : Retroknowledge.field Pcoq.Entry.t
-val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type
-
 val wit_in_clause :
   (lident Locus.clause_expr,
    lident Locus.clause_expr,
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index dc027c4041..8dad6260ae 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -545,22 +545,6 @@ END
 
 
 (**********************************************************************)
-(*spiwack : Vernac commands for retroknowledge                        *)
-
-VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF
- | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] ->
-           [ let env = Global.env () in
-             let evd = Evd.from_env env in
-             let tc,_ctx = Constrintern.interp_constr env evd c in
-             let tb,_ctx(*FIXME*) = Constrintern.interp_constr env evd b in
-             let tc = EConstr.to_constr evd tc in
-             let tb = EConstr.to_constr evd tb in
-             Global.register f tc tb ]
-END
-
-
-
-(**********************************************************************)
 (* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as
   defined by Conor McBride *)
 TACTIC EXTEND generalize_eqs
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 246acfc92e..20185363e6 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -123,7 +123,7 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
   try
     if const then
       let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(0)) params in
-      Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkInd ind) tag, ctyp
+      Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (GlobRef.IndRef ind) tag, ctyp
     else
       raise Not_found
   with Not_found ->
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 82c732c59f..c30c4f0932 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -79,7 +79,7 @@ let construct_of_constr const env tag typ =
   (* spiwack : here be a branch for specific decompilation handled by retroknowledge *)
   try
     if const then
-      ((Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkIndU indu) tag),
+      ((Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (GlobRef.IndRef ind) tag),
        typ) (*spiwack: this may need to be changed in case there are parameters in the
 	               type which may cause a constant value to have an arity.
 	               (type_constructor seems to be all about parameters actually)
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 77ab624ca5..ca7d3ec074 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -45,8 +45,8 @@ Inductive int31 : Type := I31 : digits31 int31.
 (* spiwack: Registration of the type of integers, so that the matchs in
    the functions below perform dynamic decompilation (otherwise some segfault
    occur when they are applied to one non-closed term and one closed term). *)
-Register digits as int31 bits in "coq_int31" by True.
-Register int31 as int31 type in "coq_int31" by True.
+Register digits as int31.bits.
+Register int31 as int31.type.
 
 Declare Scope int31_scope.
 Declare ML Module "int31_syntax_plugin".
@@ -345,21 +345,21 @@ Definition lor31 n m := phi_inv (Z.lor (phi n) (phi m)).
 Definition land31 n m := phi_inv (Z.land (phi n) (phi m)).
 Definition lxor31 n m := phi_inv (Z.lxor (phi n) (phi m)).
 
-Register add31 as int31 plus in "coq_int31" by True.
-Register add31c as int31 plusc in "coq_int31" by True.
-Register add31carryc as int31 pluscarryc in "coq_int31" by True.
-Register sub31 as int31 minus in "coq_int31" by True.
-Register sub31c as int31 minusc in "coq_int31" by True.
-Register sub31carryc as int31 minuscarryc in "coq_int31" by True.
-Register mul31 as int31 times in "coq_int31" by True.
-Register mul31c as int31 timesc in "coq_int31" by True.
-Register div3121 as int31 div21 in "coq_int31" by True.
-Register div31 as int31 diveucl in "coq_int31" by True.
-Register compare31 as int31 compare in "coq_int31" by True.
-Register addmuldiv31 as int31 addmuldiv in "coq_int31" by True.
-Register lor31 as int31 lor in "coq_int31" by True.
-Register land31 as int31 land in "coq_int31" by True.
-Register lxor31 as int31 lxor in "coq_int31" by True.
+Register add31 as int31.plus.
+Register add31c as int31.plusc.
+Register add31carryc as int31.pluscarryc.
+Register sub31 as int31.minus.
+Register sub31c as int31.minusc.
+Register sub31carryc as int31.minuscarryc.
+Register mul31 as int31.times.
+Register mul31c as int31.timesc.
+Register div3121 as int31.div21.
+Register div31 as int31.diveucl.
+Register compare31 as int31.compare.
+Register addmuldiv31 as int31.addmuldiv.
+Register lor31 as int31.lor.
+Register land31 as int31.land.
+Register lxor31 as int31.lxor.
 
 Definition lnot31 n := lxor31 Tn n.
 Definition ldiff31 n m := land31 n (lnot31 m).
@@ -485,5 +485,5 @@ Definition tail031 (i:int31) :=
     end)
    i On.
 
-Register head031 as int31 head0 in "coq_int31" by True.
-Register tail031 as int31 tail0 in "coq_int31" by True.
+Register head031 as int31.head0.
+Register tail031 as int31.tail0.
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 44c0159d1b..650b28ea67 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -212,8 +212,10 @@ GRAMMAR EXTEND Gram
       | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> { VernacScheme l }
       | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
 	      l = LIST1 identref SEP "," -> { VernacCombinedScheme (id, l) }
-      | IDENT "Register"; IDENT "Inline"; id = identref ->
-          { VernacRegister(id, RegisterInline) }
+      | IDENT "Register"; g = global; "as"; quid = qualid ->
+          { VernacRegister(g, RegisterRetroknowledge quid) }
+      | IDENT "Register"; IDENT "Inline"; g = global ->
+          { VernacRegister(g, RegisterInline) }
       | IDENT "Universe"; l = LIST1 identref -> { VernacUniverse l }
       | IDENT "Universes"; l = LIST1 identref -> { VernacUniverse l }
       | IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> { VernacConstraint l }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 63e9e4fe49..e15e57a003 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1161,7 +1161,11 @@ open Pputils
       | VernacRegister (id, RegisterInline) ->
         return (
           hov 2
-            (keyword "Register Inline" ++ spc() ++ pr_lident id)
+            (keyword "Register Inline" ++ spc() ++ pr_qualid id)
+        )
+      | VernacRegister (id, RegisterRetroknowledge n) ->
+        return (
+          hov 2 (keyword "Register" ++ spc () ++ pr_qualid id ++ spc () ++ keyword "as" ++ pr_qualid n)
         )
       | VernacComments l ->
         return (
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e6b3721134..28abd1e6ef 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1950,14 +1950,23 @@ let vernac_locate = function
   | LocateOther (s, qid) -> print_located_other s qid
   | LocateFile f -> locate_file f
 
-let vernac_register id r =
+let vernac_register qid r =
+  let gr = Smartlocate.global_with_alias qid in
  if Proof_global.there_are_pending_proofs () then
     user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
-  let kn = Constrintern.global_reference id.v in
-  if not (isConstRef kn) then
-    user_err Pp.(str "Register inline: a constant is expected");
   match r with
-  | RegisterInline -> Global.register_inline (destConstRef kn)
+  | RegisterInline ->
+    if not (isConstRef gr) then
+      user_err Pp.(str "Register inline: a constant is expected");
+    Global.register_inline (destConstRef gr)
+  | RegisterRetroknowledge n ->
+    let path, id = Libnames.repr_qualid n in
+    if DirPath.equal path Retroknowledge.int31_path
+    then
+      let f = Retroknowledge.(KInt31 (int31_field_of_string (Id.to_string id))) in
+      Global.register f gr
+    else
+      user_err Pp.(str "Register in unknown namespace: " ++ str (DirPath.to_string path))
 
 (********************)
 (* Proof management *)
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 11b2a7d802..ea69ed59a3 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -278,6 +278,7 @@ type extend_name =
    It will be extended with primitive inductive types and operators *)
 type register_kind =
   | RegisterInline
+  | RegisterRetroknowledge of qualid
 
 type bullet = Proof_bullet.t
 [@@ocaml.deprecated "Alias type, please use [Proof_bullet.t]"]
@@ -438,7 +439,7 @@ type nonrec vernac_expr =
   | VernacPrint of printable
   | VernacSearch of searchable * Goal_select.t option * search_restriction
   | VernacLocate of locatable
-  | VernacRegister of lident * register_kind
+  | VernacRegister of qualid * register_kind
   | VernacComments of comment list
 
   (* Proof management *)