make end2end compile

mit-plv · Jan 9, 2025 · 6ccd901 · 6ccd901
1 parent 0a82952
commit 6ccd901
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/end2end/src/end2end/End2EndLightbulb.v b/end2end/src/end2end/End2EndLightbulb.v
@@ -260,7 +260,7 @@ Proof.
   - reflexivity.
   - (* preserve invariant *)
     intros.
-    specialize (H ltac:(repeat constructor)).
+    specialize (H ltac:(repeat constructor) ltac:(repeat constructor)).
     unfold hl_inv, isReady, goodTrace, goodHlTrace in *.
     Simp.simp.
     repeat ProgramLogic.straightline.