diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v index 7f286d7a9fa12aacc86e85680eb88a815fac89fc..5b0453acbea8ca315a54ab601267fc682b811a67 100644 --- a/theories/lifetime/model/definitions.v +++ b/theories/lifetime/model/definitions.v @@ -27,8 +27,6 @@ Inductive bor_state := | Bor_in | Bor_open (q : frac) | Bor_rebor (κ : lft). -Instance bor_state_eq_dec : EqDecision bor_state. -Proof. solve_decision. Defined. Canonical bor_stateC := leibnizC bor_state. Record lft_names := LftNames { @@ -36,8 +34,6 @@ Record lft_names := LftNames { cnt_name : gname; inh_name : gname }. -Instance lft_names_eq_dec : EqDecision lft_names. -Proof. solve_decision. Defined. Canonical lft_namesC := leibnizC lft_names. Definition lft_stateR := csumR fracR unitR.