diff options
Diffstat (limited to 'theories/Init/Datatypes.v')
| -rw-r--r-- | theories/Init/Datatypes.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 1ea54e620..bab764bcb 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -120,6 +120,7 @@ Defined. Inductive BoolSpec (P Q : Prop) : bool -> Prop := | BoolSpecT : P -> BoolSpec P Q true | BoolSpecF : Q -> BoolSpec P Q false. +Hint Constructors BoolSpec. (********************************************************************) |