Skip to content
Snippets Groups Projects
Commit fb1221c5 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix typos.

parent 3bc1f853
Branches
Tags
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/base_logic/lib/cancelable_invariants.v
+ 2
− 2
View file @ fb1221c5
...@@ -37,9 +37,9 @@ Section proofs. ...@@ -37,9 +37,9 @@ Section proofs.
Global Instance cinv_persistent N γ P : Persistent (cinv N γ P). Global Instance cinv_persistent N γ P : Persistent (cinv N γ P).
Proof. rewrite /cinv; apply _. Qed. Proof. rewrite /cinv; apply _. Qed.
Global Instance cinv_own_fractionnal γ : Fractional (cinv_own γ). Global Instance cinv_own_fractional γ : Fractional (cinv_own γ).
Proof. intros ??. by rewrite -own_op. Qed. Proof. intros ??. by rewrite -own_op. Qed.
Global Instance cinv_own_as_fractionnal γ q : Global Instance cinv_own_as_fractional γ q :
AsFractional (cinv_own γ q) (cinv_own γ) q. AsFractional (cinv_own γ q) (cinv_own γ) q.
Proof. split. done. apply _. Qed. Proof. split. done. apply _. Qed.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment