diff options
Diffstat (limited to 'scheduling')
| -rw-r--r-- | scheduling/BTL_SEimpl.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index 0cbc46e6..9b48c7d2 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -1241,9 +1241,14 @@ Qed. Global Opaque option_eq_check. Hint Resolve option_eq_check_correct:wlp. -Import PTree. +Import PTree. Fixpoint PTree_eq_check' {A} (d1 d2: PTree.tree' A): ?? unit := + DO phy <~ phys_eq d1 d2;; + if phy + then + RET tt + else match d1, d2 with | Node001 r1, Node001 r2 => PTree_eq_check' r1 r2 | Node010 x1, Node010 x2 => |