From dfea5f0f6307177a9127ce29db496a819dcdb232 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Wed, 17 Jun 2020 19:53:43 +0100 Subject: Fix array semantics merge granularity. --- src/common/Coquplib.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/common/Coquplib.v') 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). -- cgit