Commit 472e32c9 authored by Joseph Tassarotti's avatar Joseph Tassarotti

Fix another typo in proofmode.

parent 7f12ce11
......@@ -730,7 +730,7 @@ Tactic Notation "iPoseProofCoreLem"
|pm_reduce;
lazymatch goal with
| |- False =>
let Htmp := pretty_ident Hnew in
let Hnew := pretty_ident Hnew in
fail "iPoseProof:" Hnew "not fresh"
| _ => tac
end];
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment