diff options
Diffstat (limited to 'src/Util/PointedProp.v')
-rw-r--r-- | src/Util/PointedProp.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Util/PointedProp.v b/src/Util/PointedProp.v index bc9626477..55cbe6d74 100644 --- a/src/Util/PointedProp.v +++ b/src/Util/PointedProp.v @@ -14,6 +14,9 @@ Definition to_prop (x : pointed_Prop) : Prop | inject p => p end. +Coercion option_pointed_Prop_of_bool (x : bool) : option pointed_Prop + := if x then Some trivial else None. + Definition and_pointed_Prop (x y : pointed_Prop) : pointed_Prop := match x, y with | trivial, y => y |