diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml
index 6d0664f6ea0f54f0f55b1005fa1cc7976364f33e..b9e595f05087b207c290ec2e6c5d4ffc070908d9 100644
--- a/src/proto_alpha/lib_protocol/script_ir_translator.ml
+++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml
@@ -1287,33 +1287,33 @@ let[@coq_axiom_with_reason "complex mutually recursive definition"] rec parse_ty
              []
              Type_namespace
              [
-               T_pair;
-               T_or;
-               T_set;
-               T_map;
-               T_list;
-               T_option;
-               T_lambda;
-               T_unit;
-               T_signature;
+               T_bls12_381_fr;
+               T_bls12_381_g1;
+               T_bls12_381_g2;
+               T_bool;
+               T_bytes;
+               T_chain_id;
                T_contract;
                T_int;
-               T_nat;
-               T_operation;
-               T_string;
-               T_bytes;
-               T_mutez;
-               T_bool;
                T_key;
                T_key_hash;
-               T_timestamp;
-               T_chain_id;
+               T_lambda;
+               T_list;
+               T_map;
+               T_mutez;
+               T_nat;
                T_never;
-               T_bls12_381_g1;
-               T_bls12_381_g2;
-               T_bls12_381_fr;
+               T_operation;
+               T_option;
+               T_or;
+               T_pair;
+               T_set;
+               T_signature;
+               T_string;
                T_ticket;
+               T_timestamp;
                T_tx_rollup_l2_address;
+               T_unit;
              ]
 
 and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_comparable_ty
@@ -4696,95 +4696,95 @@ and[@coq_axiom_with_reason "gadt"] parse_instr :
            [Seq_kind]
            Instr_namespace
            [
-             I_DROP;
-             I_DUP;
-             I_DIG;
-             I_DUG;
-             I_VIEW;
-             I_SWAP;
-             I_SOME;
-             I_UNIT;
-             I_PAIR;
-             I_UNPAIR;
+             I_ABS;
+             I_ADD;
+             I_AMOUNT;
+             I_AND;
+             I_BALANCE;
+             I_BLAKE2B;
              I_CAR;
              I_CDR;
+             I_CHECK_SIGNATURE;
+             I_COMPARE;
+             I_CONCAT;
              I_CONS;
-             I_MEM;
-             I_UPDATE;
-             I_MAP;
-             I_ITER;
-             I_GET;
-             I_GET_AND_UPDATE;
+             I_CREATE_CONTRACT;
+             I_DIG;
+             I_DIP;
+             I_DROP;
+             I_DUG;
+             I_DUP;
+             I_EDIV;
+             I_EMPTY_BIG_MAP;
+             I_EMPTY_MAP;
+             I_EMPTY_SET;
+             I_EQ;
              I_EXEC;
              I_FAILWITH;
-             I_SIZE;
-             I_CONCAT;
-             I_ADD;
-             I_SUB;
-             I_SUB_MUTEZ;
-             I_MUL;
-             I_EDIV;
-             I_OR;
-             I_AND;
-             I_XOR;
-             I_NOT;
-             I_ABS;
+             I_GE;
+             I_GET;
+             I_GET_AND_UPDATE;
+             I_GT;
+             I_HASH_KEY;
+             I_IF;
+             I_IF_CONS;
+             I_IF_LEFT;
+             I_IF_NONE;
+             I_IMPLICIT_ACCOUNT;
              I_INT;
-             I_NEG;
+             I_ITER;
+             I_JOIN_TICKETS;
+             I_KECCAK;
+             I_LAMBDA;
+             I_LE;
+             I_LEFT;
+             I_LEVEL;
+             I_LOOP;
              I_LSL;
              I_LSR;
-             I_COMPARE;
-             I_EQ;
-             I_NEQ;
              I_LT;
-             I_GT;
-             I_LE;
-             I_GE;
-             I_TRANSFER_TOKENS;
-             I_CREATE_CONTRACT;
-             I_NOW;
+             I_MAP;
+             I_MEM;
              I_MIN_BLOCK_TIME;
-             I_AMOUNT;
-             I_BALANCE;
-             I_LEVEL;
-             I_IMPLICIT_ACCOUNT;
-             I_CHECK_SIGNATURE;
-             I_BLAKE2B;
-             I_SHA256;
-             I_SHA512;
-             I_HASH_KEY;
-             I_PUSH;
+             I_MUL;
+             I_NEG;
+             I_NEQ;
+             I_NEVER;
+             I_NIL;
              I_NONE;
-             I_LEFT;
+             I_NOT;
+             I_NOW;
+             I_OPEN_CHEST;
+             I_OR;
+             I_PAIR;
+             I_PAIRING_CHECK;
+             I_PUSH;
+             I_READ_TICKET;
              I_RIGHT;
-             I_NIL;
-             I_EMPTY_SET;
-             I_DIP;
-             I_LOOP;
-             I_IF_NONE;
-             I_IF_LEFT;
-             I_IF_CONS;
-             I_EMPTY_MAP;
-             I_EMPTY_BIG_MAP;
-             I_IF;
-             I_SOURCE;
-             I_SENDER;
+             I_SAPLING_EMPTY_STATE;
+             I_SAPLING_VERIFY_UPDATE;
              I_SELF;
              I_SELF_ADDRESS;
-             I_LAMBDA;
-             I_NEVER;
-             I_VOTING_POWER;
-             I_TOTAL_VOTING_POWER;
-             I_KECCAK;
+             I_SENDER;
+             I_SHA256;
              I_SHA3;
-             I_PAIRING_CHECK;
-             I_SAPLING_EMPTY_STATE;
-             I_SAPLING_VERIFY_UPDATE;
-             I_TICKET;
-             I_READ_TICKET;
+             I_SHA512;
+             I_SIZE;
+             I_SOME;
+             I_SOURCE;
              I_SPLIT_TICKET;
-             I_JOIN_TICKETS;
-             I_OPEN_CHEST;
+             I_SUB;
+             I_SUB_MUTEZ;
+             I_SWAP;
+             I_TICKET;
+             I_TOTAL_VOTING_POWER;
+             I_TRANSFER_TOKENS;
+             I_UNIT;
+             I_UNPAIR;
+             I_UPDATE;
+             I_VIEW;
+             I_VOTING_POWER;
+             I_XOR;
            ]
 
 and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_contract :