Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it had

no particular purpose.

7 files changed, 22 insertions, 23 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 58465849c..d0da84623 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -373,7 +373,7 @@ let rec str_const c =
 		try
 		  Bstrconst (Retroknowledge.get_vm_constant_static_info
                                               (!global_env).retroknowledge
-                                              (kind_of_term f) args)
+                                              f args)
                 with NotClosed ->
 		  (* 2/ if the arguments are not all closed (this is
                         expectingly (and it is currently the case) the only
@@ -394,7 +394,7 @@ let rec str_const c =
 		  let b_args = Array.map str_const rargs in
 		  Bspecial ((Retroknowledge.get_vm_constant_dynamic_info
                                            (!global_env).retroknowledge
-                                           (kind_of_term f)),
+                                           f),
                            b_args)
               with Not_found ->
 		(* 3/ if no special behavior is available, then the compiler
@@ -415,7 +415,7 @@ let rec str_const c =
 	      try
 		Bspecial ((Retroknowledge.get_vm_constant_dynamic_info
                                            (!global_env).retroknowledge
-                                           (kind_of_term f)),
+                                           f),
                          b_args)
 	      with Not_found ->
 	        Bconstruct_app(num, nparams, arity, b_args)
@@ -430,7 +430,7 @@ let rec str_const c =
       try
 	Bspecial ((Retroknowledge.get_vm_constant_dynamic_info
                                            (!global_env).retroknowledge
-                                           (kind_of_term c)),
+                                           c),
                          [| |])
       with Not_found ->
 	let oib = lookup_mind kn !global_env in
@@ -657,7 +657,7 @@ let rec compile_constr reloc c sz cont =
       in
       compile_constr reloc a sz
       (try
-	let entry = Term.Ind ind in
+	let entry = mkInd ind in
 	Retroknowledge.get_vm_before_match_info (!global_env).retroknowledge
 	                                       entry code_sw
       with Not_found ->
@@ -689,7 +689,7 @@ and compile_const =
               falls back on its normal behavior *)
   try
     Retroknowledge.get_vm_compiling_info (!global_env).retroknowledge
-                  (kind_of_term (mkConst kn)) reloc args sz cont
+                  (mkConst kn) reloc args sz cont
   with Not_found ->
     if Int.equal nargs 0 then
       Kgetglobal (get_allias !global_env kn) :: cont
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 15db39328..4c1d9bddc 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -422,8 +422,8 @@ let unregister env field =
 	(*there is only one matching kind due to the fact that Environ.env
           is abstract, and that the only function which add elements to the
           retroknowledge is Environ.register which enforces this shape *)
-	(match retroknowledge find env field with
-	   | Ind i31t -> let i31c = Construct (i31t, 1) in
+	(match kind_of_term (retroknowledge find env field) with
+	   | Ind i31t -> let i31c = mkConstruct (i31t, 1) in
 	     {env with retroknowledge =
 		 remove (retroknowledge clear_info env i31c) field}
 	   | _ -> assert false)
@@ -479,13 +479,13 @@ fun env field value ->
   (* subfunction which shortens the (very often use) registration of binary
      operators to the reactive retroknowledge. *)
   let add_int31_binop_from_const op =
-    match value with
+    match kind_of_term value with
       | Const kn ->  retroknowledge add_int31_op env value 2
 	                               op kn
       | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant")
   in
   let add_int31_unop_from_const op =
-    match value with
+    match kind_of_term value with
       | Const kn ->  retroknowledge add_int31_op env value 1
 	                               op kn
       | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant")
@@ -497,9 +497,9 @@ fun env field value ->
        would raise Not_found. The invariant is enforced in safe_typing.ml *)
     match field with
       | KInt31 (grp, Int31Type) ->
-	  (match Retroknowledge.find rk (KInt31 (grp,Int31Bits)) with
+	  (match kind_of_term (Retroknowledge.find rk (KInt31 (grp,Int31Bits))) with
 	    | Ind i31bit_type ->
-		(match value with
+		(match kind_of_term value with
 		  | Ind i31t ->
 		      Retroknowledge.add_vm_decompile_constant_info rk
 		               value (constr_of_int31 i31t i31bit_type)
@@ -511,8 +511,8 @@ fun env field value ->
   let retroknowledge_with_reactive_info =
   match field with
     | KInt31 (_, Int31Type) ->
-        let i31c = match value with
-                     | Ind i31t -> (Construct (i31t, 1))
+        let i31c = match kind_of_term value with
+                     | Ind i31t -> mkConstruct (i31t, 1)
 		     | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type")
 	in
 	add_int31_decompilation_from_type
@@ -529,14 +529,14 @@ fun env field value ->
     | KInt31 (_, Int31Times) -> add_int31_binop_from_const Cbytecodes.Kmulint31
     | KInt31 (_, Int31TimesC) -> add_int31_binop_from_const Cbytecodes.Kmulcint31
     | KInt31 (_, Int31Div21) -> (* this is a ternary operation *)
-                                (match value with
+                                (match kind_of_term value with
 				 | Const kn ->
 				     retroknowledge add_int31_op env value 3
 	                               Cbytecodes.Kdiv21int31 kn
 				 | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant"))
     | KInt31 (_, Int31Div) -> add_int31_binop_from_const Cbytecodes.Kdivint31
     | KInt31 (_, Int31AddMulDiv) -> (* this is a ternary operation *)
-                                (match value with
+                                (match kind_of_term value with
 				 | Const kn ->
 				     retroknowledge add_int31_op env value 3
 	                               Cbytecodes.Kaddmuldivint31 kn
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 188bff626..6d0e919f8 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -282,7 +282,7 @@ let subst_structure subst = subst_structure subst do_delta_codom
 (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *)
 let add_retroknowledge mp =
   let perform rkaction env = match rkaction with
-    |Retroknowledge.RKRegister (f, (Const _ | Ind _ as e)) ->
+    |Retroknowledge.RKRegister (f, e) when (isConst e || isInd e) ->
       Environ.register env f e
     |_ ->
       Errors.anomaly ~label:"Modops.add_retroknowledge"
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 0c03e3299..632889080 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -24,7 +24,7 @@ open Term
    about a specific name.*)
 
 (* aliased type for clarity purpose*)
-type entry =  (constr, types) kind_of_term
+type entry = Constr.t
 
 (* the following types correspond to the different "things"
    the kernel can learn about. These are the fields of the proactive knowledge*)
@@ -103,8 +103,7 @@ type proactive = entry Proactive.t
 module EntryOrd =
 struct
   type t = entry
-  let make (e : entry) : constr = Obj.magic e (** WARNING: maybe to be updated. *)
-  let compare c1 c2 = Constr.compare (make c1) (make c2)
+  let compare = Constr.compare
 end
 
 module Reactive = Map.Make (EntryOrd)
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index ea2b3de24..528f6ad16 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -11,7 +11,7 @@ open Term
 type retroknowledge
 
 (** aliased type for clarity purpose*)
-type entry =  (constr, types) kind_of_term
+type entry = Constr.t
 
 (** the following types correspond to the different "things"
    the kernel can learn about.*)
diff --git a/library/global.ml b/library/global.ml
index f75c8e592..9f683b2ff 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -156,7 +156,7 @@ let type_of_global t = type_of_reference (env ()) t
 
 (* spiwack: register/unregister functions for retroknowledge *)
 let register field value by_clause =
-  globalize0 (Safe_typing.register field (kind_of_term value) by_clause)
+  globalize0 (Safe_typing.register field value by_clause)
 
 let register_inline c = globalize0 (Safe_typing.register_inline c)
 
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 8269674d7..b2fa631cd 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -71,7 +71,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 Retroknowledge.get_vm_decompile_constant_info env (Ind ind) tag),
+      ((retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkInd 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)