Remove LSLINT63CONST1 and LSRINT63CONST1 as they are unused.

6 files changed, 0 insertions, 39 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index f562c15aa8..ab6e393178 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -61,7 +61,6 @@ void init_arity () {
     arity[CHECKDIV21INT63]=
     arity[CHECKLXORINT63]=arity[CHECKLORINT63]=arity[CHECKLANDINT63]=
     arity[CHECKLSLINT63]=arity[CHECKLSRINT63]=arity[CHECKADDMULDIVINT63]=
-    arity[CHECKLSLINT63CONST1]=arity[CHECKLSRINT63CONST1]=
     arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]=
     arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]=
     arity[CHECKEQFLOAT]=arity[CHECKLTFLOAT]=arity[CHECKLEFLOAT]=
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index a124a51c7d..62683b87a6 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1497,34 +1497,6 @@ value coq_interprete
         Next;
       }
 
-      Instruct(CHECKLSLINT63CONST1) {
-        print_instr("CHECKLSLINT63CONST1");
-        if (Is_uint63(accu)) {
-          pc++;
-          Uint63_lsl1(accu);
-          Next;
-        } else {
-          *--sp = uint63_one();
-          *--sp = accu;
-          accu = Field(coq_global_data, *pc++);
-          goto apply2;
-        }
-      }
-
-      Instruct(CHECKLSRINT63CONST1) {
-        print_instr("CHECKLSRINT63CONST1");
-        if (Is_uint63(accu)) {
-          pc++;
-          Uint63_lsr1(accu);
-          Next;
-        } else {
-          *--sp = uint63_one();
-          *--sp = accu;
-          accu = Field(coq_global_data, *pc++);
-          goto apply2;
-        }
-      }
-
       Instruct (CHECKADDMULDIVINT63) {
         print_instr("CHECKADDMULDIVINT63");
         CheckInt3();
diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h
index 13568957c2..dd9b9e55be 100644
--- a/kernel/byterun/coq_uint63_emul.h
+++ b/kernel/byterun/coq_uint63_emul.h
@@ -119,12 +119,8 @@ DECLARE_BINOP(lor)
 #define Uint63_lor(x, y) CALL_BINOP(lor, x, y)
 DECLARE_BINOP(lsl)
 #define Uint63_lsl(x, y) CALL_BINOP(lsl, x, y)
-DECLARE_UNOP(lsl1)
-#define Uint63_lsl1(x) CALL_UNOP(lsl1, x)
 DECLARE_BINOP(lsr)
 #define Uint63_lsr(x, y) CALL_BINOP(lsr, x, y)
-DECLARE_UNOP(lsr1)
-#define Uint63_lsr1(x) CALL_UNOP(lsr1, x)
 DECLARE_BINOP(lt)
 #define Uint63_lt(r, x, y) CALL_RELATION(r, lt, x, y)
 DECLARE_BINOP(lxor)
diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h
index 27696e8856..731ae8f46e 100644
--- a/kernel/byterun/coq_uint63_native.h
+++ b/kernel/byterun/coq_uint63_native.h
@@ -55,8 +55,6 @@
   else \
     accu = uint63_zero; \
   }while(0)
-#define Uint63_lsl1(x) (accu = (value)((((uint64_t)(x)-1) << 1) +1))
-#define Uint63_lsr1(x) (accu = (value)(((uint64_t)(x) >> 1) |1))
 
 /* addmuldiv(p,x,y) = x * 2^p + y / 2 ^ (63 - p) */
 /* (modulo 2^63) for p <= 63 */
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index e2932ec330..ca9985d079 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -120,8 +120,6 @@ let opcodes =
     "CHECKLSLINT63";
     "CHECKLSRINT63";
     "CHECKADDMULDIVINT63";
-    "CHECKLSLINT63CONST1";
-    "CHECKLSRINT63CONST1";
     "CHECKEQINT63";
     "CHECKLTINT63";
     "CHECKLEINT63";
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index 988611df3e..4f2cbc4262 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -206,9 +206,7 @@ let () =
   Callback.register "uint63 leq" le;
   Callback.register "uint63 lor" l_or;
   Callback.register "uint63 lsl" l_sl;
-  Callback.register "uint63 lsl1" (fun x -> l_sl x Int64.one);
   Callback.register "uint63 lsr" l_sr;
-  Callback.register "uint63 lsr1" (fun x -> l_sr x Int64.one);
   Callback.register "uint63 lt" lt;
   Callback.register "uint63 lxor" l_xor;
   Callback.register "uint63 mod" rem;