diff options
Diffstat (limited to 'riscV/Asmgenproof1.v')
| -rw-r--r-- | riscV/Asmgenproof1.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 0b1abe2a..35c5b9d6 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -377,7 +377,7 @@ Proof. rewrite <- Float32.cmp_swap. auto. Qed. -(* TODO UNUSUED ? Remark branch_on_X31: +(* TODO gourdinl UNUSUED ? Remark branch_on_X31: forall normal lbl (rs: regset) m b, rs#X31 = Val.of_bool (eqb normal b) -> exec_instr ge fn (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) rs m = |