diff options
Diffstat (limited to 'theories/Bool/Sumbool.v')
| -rw-r--r-- | theories/Bool/Sumbool.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v index 52605a4667..49feda15ea 100644 --- a/theories/Bool/Sumbool.v +++ b/theories/Bool/Sumbool.v @@ -19,6 +19,7 @@ Definition sumbool_of_bool : forall b:bool, {b = true} + {b = false}. intros b; destruct b; auto. Defined. +#[global] Hint Resolve sumbool_of_bool: bool. Definition bool_eq_rec : @@ -57,7 +58,9 @@ Section connectives. End connectives. +#[global] Hint Resolve sumbool_and sumbool_or: core. +#[global] Hint Immediate sumbool_not : core. (** Any decidability function in type [sumbool] can be turned into a function |