diff options
Diffstat (limited to 'src/LegacyArithmetic/InterfaceProofs.v')
| -rw-r--r-- | src/LegacyArithmetic/InterfaceProofs.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/LegacyArithmetic/InterfaceProofs.v b/src/LegacyArithmetic/InterfaceProofs.v index 9ef97fa55..33917e00d 100644 --- a/src/LegacyArithmetic/InterfaceProofs.v +++ b/src/LegacyArithmetic/InterfaceProofs.v @@ -99,8 +99,9 @@ Global Instance decode_proj n W (dec : W -> Z) : @decode n W {| decode := dec |} =~> dec. Proof. reflexivity. Qed. -Global Instance decode_if_bool n W (decode : decoder n W) (b : bool) x y - : decode (if b then x else y) +Global Instance decode_if_bool n W (decode : decoder n W) + : forall (b : bool) x y, + decode (if b then x else y) =~> if b then decode x else decode y. Proof. destruct b; reflexivity. Qed. |