From 2f46b5c2420fec2d349a1ac192c8877d7737b72e Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 3 Dec 2021 09:31:59 +0100
Subject: physical equality

---
 scheduling/BTL_SEimpl.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'scheduling')

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 =>
-- 
cgit