diff --git a/tests/proofmode.v b/tests/proofmode.v index adfc177806e26664ff802370167e7eb40a3d4001..85903527afee202cdab0dad918da1d8552b72c69 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -158,7 +158,7 @@ Proof. iIntros "H". let H1 := iFresh in let H2 := iFresh in - let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in + let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in iDestruct "H" as pat. iFrame. Qed.