diff options
author | James Pollard <james@pollard.dev> | 2020-06-17 19:53:43 +0100 |
---|---|---|
committer | James Pollard <james@pollard.dev> | 2020-06-17 19:53:43 +0100 |
commit | dfea5f0f6307177a9127ce29db496a819dcdb232 (patch) | |
tree | 1f8c9784e145dc676c037f2376021af7be9e3bff /src/common | |
parent | 044a68b1b215125e2651c637f28c794536d27ba5 (diff) | |
download | vericert-kvx-dfea5f0f6307177a9127ce29db496a819dcdb232.tar.gz vericert-kvx-dfea5f0f6307177a9127ce29db496a819dcdb232.zip |
Fix array semantics merge granularity.
Diffstat (limited to 'src/common')
-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). |