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

diff --git a/src/HaskCore.v b/src/HaskCore.v
index 2242e48..e9f3929 100644
--- a/src/HaskCore.v
+++ b/src/HaskCore.v
@@ -42,9 +42,6 @@ Extract Inductive CoreBind =>
 (* extracts the Name from a CoreVar *)
 Variable coreVarCoreName    : CoreVar -> CoreName.   Extract Inlined Constant coreVarCoreName  => "Var.varName".
 
-Variable coretype_eq_dec : forall (c1 c2:CoreType), sumbool (eq c1 c2) (not (eq c1 c2)).
-  Extract Inlined Constant coretype_eq_dec => "Type.coreEqType".
-
 Extract Constant ArrowTyCon           => "Type.funTyCon".     (* Figure 7, (->) *)
 Extract Constant CoFunConst           => "TyCon.TyCon".                        Extraction Implicit CoFunConst [ 1 ].
 Extract Constant TyFunConst           => "TyCon.TyCon".                        Extraction Implicit TyFunConst [ 1 ].
@@ -59,18 +56,4 @@ Variable hetmet_brak_name   : CoreName.              Extract Inlined Constant he
 (* the magic wired-in name for the modal type elimination form *)
 Variable hetmet_esc_name    : CoreName.              Extract Inlined Constant hetmet_esc_name  => "PrelNames.hetmet_esc_name".
 
-(* detects our crude Core-encoding of modal type introduction/elimination forms *)
-Definition isBrak (ce:CoreExpr CoreVar) : ??CoreVar :=
-match ce with
-  | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
-    => if coreName_eq hetmet_brak_name (coreVarCoreName v) then Some ec else None
-  | _ => None
-end.
-Definition isEsc (ce:CoreExpr CoreVar) : ??CoreVar :=
-match ce with
-  | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
-    => if coreName_eq hetmet_esc_name (coreVarCoreName v) then Some ec else None
-  | _ => None
-end.
-