diff options
Diffstat (limited to 'theories/Bool')
| -rwxr-xr-x | theories/Bool/DecBool.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v index 8a15e7624..2a0b2063d 100755 --- a/theories/Bool/DecBool.v +++ b/theories/Bool/DecBool.v @@ -11,7 +11,7 @@ Set Implicit Arguments. Definition ifdec (A B:Prop) (C:Set) (H:{A} + {B}) (x y:C) : C := - if H then fun _ => x else fun _ => y. + if H then x else y. Theorem ifdec_left : |