1 files changed, 12 insertions, 1 deletions
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
index 89616c5f..8a45e973 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -35,7 +35,18 @@ enum instructions {
   CONST0, CONST1, CONST2, CONST3, CONSTINT,
   PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT,
   ACCUMULATE, ACCUMULATECOND, 
-  MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, STOP
+  MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, 
+/* spiwack: */
+  BRANCH,
+  ADDINT31, ADDCINT31, ADDCARRYCINT31,
+  SUBINT31, SUBCINT31, SUBCARRYCINT31,
+  MULCINT31, MULINT31, DIV21INT31, DIVINT31,
+  ADDMULDIVINT31, COMPAREINT31, 
+  HEAD0INT31, TAIL0INT31,
+  ISCONST, ARECONST,
+  COMPINT31, DECOMPINT31,
+/* /spiwack  */
+  STOP
 };
 
 #endif /* _COQ_INSTRUCT_ */