Commit 463474fb by Robbert Krebbers

Rename `frag_auth_op` into `frac_auth_frag_op` (the old name was inconsistent).

`sed -i 's/frag_auth_op/frac_auth_frag_op/g' $(find -name "*.v")`
parent e67830a6
Pipeline #8854 passed with stage
in 3 minutes 49 seconds
......@@ -22,6 +22,8 @@ Changes in Coq:
- `IntoLaterN'``IntoLaterN` (this one _should_ strip a later)
- `IntoLaterNEnv``MaybeIntoLaterNEnv`
- `IntoLaterNEnvs``MaybeIntoLaterNEnvs`
* Rename:
- `frag_auth_op``frac_auth_frag_op`
* `namespaces` has been moved to std++.
## Iris 3.1.0 (released 2017-12-19)
......
......@@ -81,13 +81,13 @@ Section frac_auth.
Lemma frac_auth_frag_valid q a : (!{q} a) q a.
Proof. done. Qed.
Lemma frag_auth_op q1 q2 a1 a2 : !{q1+q2} (a1 a2) !{q1} a1 !{q2} a2.
Lemma frac_auth_frag_op q1 q2 a1 a2 : !{q1+q2} (a1 a2) !{q1} a1 !{q2} a2.
Proof. done. Qed.
Lemma frac_auth_frag_validN_op_1_l n q a b : {n} (!{1} a !{q} b) False.
Proof. rewrite -frag_auth_op frac_auth_frag_validN=> -[/exclusiveN_l []]. Qed.
Proof. rewrite -frac_auth_frag_op frac_auth_frag_validN=> -[/exclusiveN_l []]. Qed.
Lemma frac_auth_frag_valid_op_1_l q a b : (!{1} a !{q} b) False.
Proof. rewrite -frag_auth_op frac_auth_frag_valid=> -[/exclusive_l []]. Qed.
Proof. rewrite -frac_auth_frag_op frac_auth_frag_valid=> -[/exclusive_l []]. Qed.
Global Instance is_op_frac_auth (q q1 q2 : frac) (a a1 a2 : A) :
IsOp q q1 q2 IsOp a a1 a2 IsOp' (!{q} a) (!{q1} a1) (!{q2} a2).
......@@ -97,7 +97,7 @@ Section frac_auth.
CoreId a IsOp q q1 q2 IsOp' (!{q} a) (!{q1} a) (!{q2} a).
Proof.
rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
by rewrite -frag_auth_op -core_id_dup.
by rewrite -frac_auth_frag_op -core_id_dup.
Qed.
Lemma frac_auth_update q a b a' b' :
......
......@@ -105,7 +105,7 @@ Section contrib_spec.
(** The main proofs. *)
Lemma ccounter_op γ q1 q2 n1 n2 :
ccounter γ (q1 + q2) (n1 + n2) ⊣⊢ ccounter γ q1 n1 ccounter γ q2 n2.
Proof. by rewrite /ccounter frag_auth_op -own_op. Qed.
Proof. by rewrite /ccounter frac_auth_frag_op -own_op. Qed.
Lemma newcounter_contrib_spec (R : iProp Σ) :
{{{ True }}} newcounter #()
......
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