+
+{- -- used for extracting strings WITHOUT the patch for Coq
+bin2ascii =
+ (\ b0 b1 b2 b3 b4 b5 b6 b7 ->
+ let f b i = if b then 1 `shiftL` i else 0
+ in Data.Char.chr (f b0 0 .|. f b1 1 .|. f b2 2 .|. f b3 3 .|. f b4 4 .|. f b5 5 .|. f b6 6 .|. f b7 7))
+-}
+
+-- I'm leaving this here (commented out) in case I ever need it again)
+--checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
+--checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)