diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-03 09:31:59 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-03 09:31:59 +0100 |
| commit | 2f46b5c2420fec2d349a1ac192c8877d7737b72e (patch) | |
| tree | ff3f8206d120d7ef207f523fc0c7ff88a702676f /scheduling | |
| parent | a781244930ababd25e40c40e8df8bd437f3fbf8c (diff) | |
| download | compcert-kvx-2f46b5c2420fec2d349a1ac192c8877d7737b72e.tar.gz compcert-kvx-2f46b5c2420fec2d349a1ac192c8877d7737b72e.zip | |
physical equality
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 => |