Merge pull request #6 from ppedrot/hint-locality-error

mit-pdos · Jun 29, 2022 · a6a5aa0 · a6a5aa0
2 parents 24fb544 + c6b4078
commit a6a5aa0
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 2 deletions.
diff --git a/src/Examples/ReplicatedDisk/ReplicatedDiskImpl.v b/src/Examples/ReplicatedDisk/ReplicatedDiskImpl.v
@@ -546,6 +546,7 @@ Module ReplicatedDisk.
     - exfalso; apply index_not_none in Heqo; auto.
   Qed.
 
+#[global]
   Hint Rewrite assign_maybe_same using (solve [ auto ]) : array.
   Global Hint Resolve PeanoNat.Nat.lt_neq : core.
   Global Hint Resolve disks_eq_inbounds : core.

diff --git a/vendor/array b/vendor/array
diff --git a/vendor/classes b/vendor/classes