Updated hahnExt dependency to 0.9.1

weakmemory · Sep 30, 2023 · 798b81a · 798b81a
1 parent d8e1e2b
commit 798b81a
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git a/.nix/config.nix b/.nix/config.nix
@@ -34,21 +34,21 @@
   bundles."8.16"= {
     coqPackages.coq.override.version = "8.16";
     coqPackages.hahn.override.version = "master";
-    coqPackages.hahnExt.override.version = "master";
+    coqPackages.hahnExt.override.version = "0.9.1";
     coqPackages.sflib.override.version = "master";
     coqPackages.promising-lib.override.version = "master";
   };
   bundles."8.17"= {
     coqPackages.coq.override.version = "8.17";
     coqPackages.hahn.override.version = "master";
-    coqPackages.hahnExt.override.version = "master";
+    coqPackages.hahnExt.override.version = "0.9.1";
     coqPackages.sflib.override.version = "master";
     coqPackages.promising-lib.override.version = "master";
   };
   bundles."8.18"= {
     coqPackages.coq.override.version = "8.18";
     coqPackages.hahn.override.version = "master";
-    coqPackages.hahnExt.override.version = "master";
+    coqPackages.hahnExt.override.version = "0.9.1";
     coqPackages.sflib.override.version = "master";
     coqPackages.promising-lib.override.version = "master";
   };

diff --git a/src/travorder/TraversalOrder.v b/src/travorder/TraversalOrder.v
@@ -479,7 +479,7 @@ Section TravLabel.
 
   Lemma RFSBFINAR WF WFSC CONS : event ↑ (RF^? ⨾ SB^? ⨾ FWBOB) ⊆ ar⁺.
   Proof using.
-    rewrite !collect_rel_seq, !collect_rel_cr.
+    rewrite !collect_rel_seqi, !collect_rel_cr.
     rewrite ERF, eSB_in_sb_sc_ct, EFWBOB. rewrite cr_of_cr.
     rewrite cr_of_ct. apply rf_sb_sc_rt_sb_fwbob_in_ar; auto.
     apply CONS.
@@ -559,7 +559,7 @@ Section TravLabel.
       clear; basic_solver 1. }
 
     eapply collect_rel_acyclic with (f:=event).
-    rewrite collect_rel_seq, collect_rel_ct.
+    rewrite collect_rel_seqi, collect_rel_ct.
     rewrite RFSBFINAR; auto. rewrite ct_of_ct.
     rewrite EAR.
     arewrite (ar ⊆ ar ∪ rf ⨾ ppo ∩ same_loc) at 1.