diff options
Diffstat (limited to 'riscV/ExpansionOracle.ml')
-rw-r--r-- | riscV/ExpansionOracle.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 39b8f367..41a2227b 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -327,7 +327,7 @@ let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 k = insn :: (if normal' then Icond (CEbnew (Some false), [ r2p (); r2p () ], succ1, succ2, info) - else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info)) (* TODO gourdinl Maybe incorrect *) + else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info)) :: k let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ] |