Skip to content

Commit 41e06a1

Browse files
committed
Adapt to float changes
1 parent 6052a52 commit 41e06a1

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

  • rocq-skylabs-brick/theories/lang/cpp/logic

rocq-skylabs-brick/theories/lang/cpp/logic/expr.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -610,7 +610,7 @@ Module Type Expr.
610610
Definition wp_init_binop_floating_spaceship_body ty f
611611
(a b : float_type.car f) (addr : ptr) (free : FreeTemps.t) Q : mpred :=
612612
wp_init_comparison_category_from_global std_partial_ordering
613-
(fun cls => partial_ordering_result_name cls (float_value.value_compare f a b))
613+
(fun cls => partial_ordering_result_name cls (float_value.value_compare a b))
614614
ty addr free Q.
615615

616616

0 commit comments

Comments
 (0)