Skip to content
Snippets Groups Projects
Commit 31a68951 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

These EqDecision instances are not needed.

parent ae3a4b2d
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
theories/lifetime/model/definitions.v
+ 0
− 4
View file @ 31a68951
...@@ -27,8 +27,6 @@ Inductive bor_state := ...@@ -27,8 +27,6 @@ Inductive bor_state :=
| Bor_in | Bor_in
| Bor_open (q : frac) | Bor_open (q : frac)
| Bor_rebor (κ : lft). | Bor_rebor (κ : lft).
Instance bor_state_eq_dec : EqDecision bor_state.
Proof. solve_decision. Defined.
Canonical bor_stateC := leibnizC bor_state. Canonical bor_stateC := leibnizC bor_state.
Record lft_names := LftNames { Record lft_names := LftNames {
...@@ -36,8 +34,6 @@ Record lft_names := LftNames { ...@@ -36,8 +34,6 @@ Record lft_names := LftNames {
cnt_name : gname; cnt_name : gname;
inh_name : gname inh_name : gname
}. }.
Instance lft_names_eq_dec : EqDecision lft_names.
Proof. solve_decision. Defined.
Canonical lft_namesC := leibnizC lft_names. Canonical lft_namesC := leibnizC lft_names.
Definition lft_stateR := csumR fracR unitR. Definition lft_stateR := csumR fracR unitR.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment