Skip to content
Snippets Groups Projects
Commit 1023ccf7 authored by Dan Frumin's avatar Dan Frumin
Browse files

Fix a proof for an older version

parent 19e1199c
No related branches found
No related tags found
No related merge requests found
Pipeline #83978 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
iris/algebra/local_updates.v
+ 1
− 1
View file @ 1023ccf7
...@@ -154,7 +154,7 @@ Proof. ...@@ -154,7 +154,7 @@ Proof.
eapply Hupd, Hg; eauto. eapply Hupd, Hg; eauto.
- specialize (Hupd i). - specialize (Hupd i).
rewrite local_update_unital in Hupd. rewrite local_update_unital in Hupd.
eapply Hupd; eauto. eapply Hupd, Hg; eauto.
Qed. Qed.
(** * Product *) (** * Product *)
......
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