Fix array semantics merge granularity.

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).