X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskWeakTypes.v;h=56c2f48c0f3c12e1e915241455ee1cfb5f60d45a;hb=5c493a75fbaf8454d8a21e55edc5b193e2c5879c;hp=82cf8ad2624b44b41627f1968d7b41d6d9f2d7e9;hpb=6232ffa2805211654c6ff40a9852d7fc312382d2;p=coq-hetmet.git

diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v
index 82cf8ad..56c2f48 100644
--- a/src/HaskWeakTypes.v
+++ b/src/HaskWeakTypes.v
@@ -120,9 +120,7 @@ Definition compare_weakTypes (w1 w2:WeakType) :=
     then true
     else false.
 
-(* Coq's "decide equality" can't cope here; we have to cheat for now *)
-Axiom compare_weakTypes_axiom : forall w1 w2, if compare_weakTypes w1 w2 then w1=w2 else not (w1=w2).
-
+(*
 Instance EqDecidableWeakType : EqDecidable WeakType.
   apply Build_EqDecidable.
   intros.
@@ -133,6 +131,7 @@ Instance EqDecidableWeakType : EqDecidable WeakType.
   left; auto.
   right; auto.
   Defined.
+*)
 
 Instance WeakTypeToString : ToString WeakType :=
   { toString := coreTypeToString ○ weakTypeToCoreType }.