aboutsummaryrefslogtreecommitdiff
path: root/src/Util/PointedProp.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/PointedProp.v')
-rw-r--r--src/Util/PointedProp.v3
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