Added WeakVar, a separate variable representation for HaskWeak

[coq-hetmet.git] / src / General.v

diff --git a/src/General.v b/src/General.v
index ad8e590..c78daa1 100644 (file)
--- 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.