Commit 46595d5c authored by Dan Frumin's avatar Dan Frumin Committed by Ralf Jung
Browse files

`Later_inj` -> `Next_inj`.

parent ec0acc9c
......@@ -19,6 +19,7 @@ lemma.
* Equip `frac_agree` with support for `dfrac` and rename it to `dfrac_agree`.
The old `to_frac_agree` and its lemmas still exist, except that the
`frac_agree_op_valid` lemmas are made bi-directional.
* Rename typeclass instance `Later_inj` -> `Next_inj`.
**Changes in `bi`:**
......@@ -1170,7 +1170,7 @@ Section later.
Global Instance Next_contractive : Contractive (@Next A).
Proof. by intros [|n] x y. Qed.
Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
Global Instance Next_inj n : Inj (dist n) (dist (S n)) (@Next A).
Proof. by intros x y. Qed.
Lemma Next_uninj x : a, x Next a.
Supports Markdown
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