diff options
Diffstat (limited to 'src/common/Coquplib.v')
-rw-r--r-- | src/common/Coquplib.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index fd0987b..675ad23 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -47,6 +47,7 @@ Ltac clear_obvious := repeat match goal with | [ H : ex _ |- _ ] => invert H | [ H : ?C _ = ?C _ |- _ ] => invert H + | [ H : _ /\ _ |- _ ] => invert H end. Ltac simplify := simpl in *; clear_obvious; simpl in *; try discriminate. @@ -81,6 +82,12 @@ Definition bind {A B : Type} (f : option A) (g : A -> option B) : option B := | _ => None end. +Definition join {A : Type} (a : option (option A)) : option A := + match a with + | None => None + | Some a' => a' + end. + Module Notation. Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200). |