From 31a689516cb325055c75534476f152d9238d5e3b Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 3 Aug 2017 10:21:59 +0200
Subject: [PATCH] These EqDecision instances are not needed.
---
theories/lifetime/model/definitions.v | 4 ----
1 file changed, 4 deletions(-)
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 7f286d7a..5b0453ac 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.
--
GitLab