From 4be2dd481c783bed7c09086b647d860e42b7ea9f Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 7 Sep 2018 11:18:28 +0200
Subject: Retroknowledge.KInt31: remove the (unused) group parameter

---
 kernel/environ.ml         |  4 ++--
 kernel/retroknowledge.ml  |  2 +-
 kernel/retroknowledge.mli |  2 +-
 kernel/safe_typing.ml     | 40 ++++++++++++++++++++--------------------
 4 files changed, 24 insertions(+), 24 deletions(-)

(limited to 'kernel')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index e7efa5e2c9..64c93a2607 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -695,10 +695,10 @@ let register_one env field entry =
 (* [register env field entry] may register several fields when needed *)
 let register env field entry =
   match field with
-    | KInt31 (grp, Int31Type) ->
+    | KInt31 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
+        register_one (register_one env (KInt31 Int31Constructor) i31c) field entry
     | field -> register_one env field entry
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 34f62defb8..0d1bb1e586 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -53,7 +53,7 @@ type int31_field =
   | Int31Lxor
 
 type field =
-  | KInt31 of string*int31_field
+  | KInt31 of int31_field
 
 
 (* record representing all the flags of the internal state of the kernel *)
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 02d961d893..6b2c74e9df 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -46,7 +46,7 @@ type int31_field =
   | Int31Lxor
 
 type field =
-  | KInt31 of string*int31_field
+  | KInt31 of int31_field
 
 (** This type represent an atomic action of the retroknowledge. It
    is stored in the compiled libraries 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 6c87ff570f..15f972afcf 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -992,12 +992,12 @@ fun rk value field ->
   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
@@ -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
 
-- 
cgit v1.2.3


From ab2560233f2e6fc8c26853af6991533d8d335e16 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 7 Sep 2018 11:34:32 +0200
Subject: Retroknowledge: remove the (unused) by clause

---
 kernel/safe_typing.ml  | 4 ++--
 kernel/safe_typing.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 15f972afcf..95eea2d6b0 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
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 502e2970a1..2f83e71726 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 -> Retroknowledge.entry -> safe_transformer0
 
 val register_inline : Constant.t -> safe_transformer0
 
-- 
cgit v1.2.3


From 42bed627c4a1c5a1ecf59d4865fc872b5eee7290 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 7 Sep 2018 12:22:17 +0200
Subject: Retroknowledge: simpler parsing rules

---
 kernel/retroknowledge.ml  | 27 +++++++++++++++++++++++++++
 kernel/retroknowledge.mli |  2 ++
 2 files changed, 29 insertions(+)

(limited to 'kernel')

diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 0d1bb1e586..2ed846d852 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -55,6 +55,33 @@ type int31_field =
 type 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)
 
 (* record representing all the flags of the internal state of the kernel *)
 type flags = {fastcomputation : bool}
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 6b2c74e9df..1436f23739 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -48,6 +48,8 @@ type int31_field =
 type field =
   | KInt31 of int31_field
 
+val int31_field_of_string : string -> int31_field
+
 (** 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
-- 
cgit v1.2.3


From 2ec78477c720ba3a5343b49f25cfa9c1639adbba Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 7 Sep 2018 17:34:11 +0200
Subject: Retroknowledge: use GlobRef.t instead of Constr.t as entry

---
 kernel/clambda.ml         | 13 +++++++------
 kernel/environ.ml         | 16 ++++++++--------
 kernel/environ.mli        |  2 +-
 kernel/modops.ml          |  2 +-
 kernel/nativelambda.ml    | 33 +++++++++++++++++----------------
 kernel/retroknowledge.ml  | 17 ++++-------------
 kernel/retroknowledge.mli | 29 +++++++++++++----------------
 kernel/safe_typing.ml     | 16 ++++++++--------
 kernel/safe_typing.mli    |  2 +-
 9 files changed, 60 insertions(+), 70 deletions(-)

(limited to 'kernel')

diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 961036d3c5..75cf6b747d 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -659,11 +659,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 *)
@@ -721,7 +721,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 ->
@@ -734,6 +734,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,
@@ -748,7 +749,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
@@ -769,7 +770,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 *)
@@ -782,7 +783,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 64c93a2607..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 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 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 2ed846d852..c1a8820bf0 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
@@ -95,19 +92,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 :
@@ -154,7 +145,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 1436f23739..1fc3cfb817 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 =
@@ -55,7 +52,7 @@ val int31_field_of_string : string -> int31_field
    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 *)
@@ -66,7 +63,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
@@ -75,7 +72,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 _ )
@@ -83,45 +80,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. *)
@@ -163,4 +160,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 95eea2d6b0..9d302c69fb 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -977,16 +977,16 @@ 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
@@ -1002,14 +1002,14 @@ fun rk value field ->
               (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.")
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 2f83e71726..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 -> safe_transformer0
+  field -> GlobRef.t -> safe_transformer0
 
 val register_inline : Constant.t -> safe_transformer0
 
-- 
cgit v1.2.3


From 736842d4cde09c667837dee8a633ff98ecf6a820 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 10 Sep 2018 13:20:39 +0200
Subject: Register: simpler syntax

---
 kernel/retroknowledge.ml  | 2 ++
 kernel/retroknowledge.mli | 2 ++
 2 files changed, 4 insertions(+)

(limited to 'kernel')

diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index c1a8820bf0..e51c25c06b 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -80,6 +80,8 @@ let int31_field_of_string =
   | "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}
 
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 1fc3cfb817..0a2ef5300e 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -47,6 +47,8 @@ type 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
-- 
cgit v1.2.3