Skip to content

Commit bb97b5c

Browse files
committed
Remove comments
1 parent 471012e commit bb97b5c

File tree

1 file changed

+0
-1
lines changed

1 file changed

+0
-1
lines changed

ArchSemArm/VMPromising.v

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1050,7 +1050,6 @@ Module TLB.
10501050
(time : nat)
10511051
(va : bv 64)
10521052
(ttbr : reg) : result string (t * bool) :=
1053-
(* make an incremental update *)
10541053
fold_left (λ prev lvl,
10551054
'(tlb_prev, is_changed_prev) ← prev;
10561055
'(tlb_new, is_changed) ← va_fill tlb_prev ts init mem time lvl va ttbr;

0 commit comments

Comments
 (0)