diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_instr_kinds.v | 37 |
1 files changed, 20 insertions, 17 deletions
diff --git a/lib/coq/Sail2_instr_kinds.v b/lib/coq/Sail2_instr_kinds.v index 85d78226..d03d5e63 100644 --- a/lib/coq/Sail2_instr_kinds.v +++ b/lib/coq/Sail2_instr_kinds.v @@ -153,28 +153,31 @@ Inductive a64_barrier_type := Inductive barrier_kind := (* Power barriers *) - Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync + | Barrier_Sync : unit -> barrier_kind + | Barrier_LwSync : unit -> barrier_kind + | Barrier_Eieio : unit -> barrier_kind + | Barrier_Isync : unit -> barrier_kind (* AArch64 barriers *) - | Barrier_DMB (*: a64_barrier_domain -> a64_barrier_type -> barrier_kind*) - | Barrier_DSB (*: a64_barrier_domain -> a64_barrier_type -> barrier_kind*) - | Barrier_ISB + | Barrier_DMB : a64_barrier_domain -> a64_barrier_type -> barrier_kind + | Barrier_DSB : a64_barrier_domain -> a64_barrier_type -> barrier_kind + | Barrier_ISB : unit -> barrier_kind (* | Barrier_TM_COMMIT*) (* MIPS barriers *) - | Barrier_MIPS_SYNC + | Barrier_MIPS_SYNC : unit -> barrier_kind (* RISC-V barriers *) - | Barrier_RISCV_rw_rw - | Barrier_RISCV_r_rw - | Barrier_RISCV_r_r - | Barrier_RISCV_rw_w - | Barrier_RISCV_w_w - | Barrier_RISCV_w_rw - | Barrier_RISCV_rw_r - | Barrier_RISCV_r_w - | Barrier_RISCV_w_r - | Barrier_RISCV_tso - | Barrier_RISCV_i + | Barrier_RISCV_rw_rw : unit -> barrier_kind + | Barrier_RISCV_r_rw : unit -> barrier_kind + | Barrier_RISCV_r_r : unit -> barrier_kind + | Barrier_RISCV_rw_w : unit -> barrier_kind + | Barrier_RISCV_w_w : unit -> barrier_kind + | Barrier_RISCV_w_rw : unit -> barrier_kind + | Barrier_RISCV_rw_r : unit -> barrier_kind + | Barrier_RISCV_r_w : unit -> barrier_kind + | Barrier_RISCV_w_r : unit -> barrier_kind + | Barrier_RISCV_tso : unit -> barrier_kind + | Barrier_RISCV_i : unit -> barrier_kind (* X86 *) - | Barrier_x86_MFENCE. + | Barrier_x86_MFENCE : unit -> barrier_kind. Scheme Equality for barrier_kind. (* |