Retroknowledge.KInt31: remove the (unused) group parameter

6 files changed, 45 insertions, 52 deletions

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
 
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 38600695dc..a9133512e0 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -345,11 +345,7 @@ let pr_r_int31_field i31f =
 
 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
+  | Retroknowledge.KInt31 i31f -> pr_r_int31_field i31f
 
 VERNAC ARGUMENT EXTEND retroknowledge_int31
 PRINTED BY pr_r_int31_field
@@ -381,8 +377,5 @@ 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) ]
+| [ retroknowledge_int31 (i) ] -> [ Retroknowledge.KInt31 i ]
 END
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 77ab624ca5..5c1c5d794d 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 by True.
+Register int31 as int31 type by True.
 
 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 by True.
+Register add31c as int31 plusc by True.
+Register add31carryc as int31 pluscarryc by True.
+Register sub31 as int31 minus by True.
+Register sub31c as int31 minusc by True.
+Register sub31carryc as int31 minuscarryc by True.
+Register mul31 as int31 times by True.
+Register mul31c as int31 timesc by True.
+Register div3121 as int31 div21 by True.
+Register div31 as int31 diveucl by True.
+Register compare31 as int31 compare by True.
+Register addmuldiv31 as int31 addmuldiv by True.
+Register lor31 as int31 lor by True.
+Register land31 as int31 land by True.
+Register lxor31 as int31 lxor by True.
 
 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 by True.
+Register tail031 as int31 tail0 by True.