X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneral.v;h=c78daa1a4253c3569a2edc0932833b2b17d6d0e3;hp=ad8e59092407035fc3daff58b2b4c5e7a767d6df;hb=5a0761840d89b82cdacb0bf9215fd41aba847b68;hpb=a5cc4e8d9bbdb4b462de09a221f958bf3020895e

diff --git a/src/General.v b/src/General.v
index ad8e590..c78daa1 100644
--- a/src/General.v
+++ b/src/General.v
@@ -17,7 +17,6 @@ Require Import Omega.
 Class EqDecidable (T:Type) :=
 { eqd_type           := T
 ; eqd_dec            :  forall v1 v2:T, sumbool (v1=v2) (not (v1=v2))
-; eqd_dec_reflexive  :  forall v, (eqd_dec v v) = (left _ (refl_equal _))
 }.
 Coercion eqd_type : EqDecidable >-> Sortclass.