-Variable CoreName : Type. Extract Inlined Constant CoreName => "Name.Name".
-Variable coreName_eq : forall (a b:CoreName), sumbool (a=b) (not (a=b)). Extract Inlined Constant coreName_eq => "(==)".
-Axiom coreName_eq_refl : ∀ v, (coreName_eq v v)=(left _ (refl_equal v)).
-Instance CoreNameEqDecidable : EqDecidable CoreName :=
-{ eqd_dec := coreName_eq
-}.
-
-Inductive CoreIPName : Type -> Type := . Extract Inductive CoreIPName => "CoreSyn.IPName" [ ].
+Variable TyCon : Type. Extract Inlined Constant TyCon => "TyCon.TyCon".
+Variable CoreDataCon : Type. Extract Inlined Constant CoreDataCon => "DataCon.DataCon".
+Variable CoreName : Type. Extract Inlined Constant CoreName => "Name.Name".
+Variable CoreCoercion : Type. Extract Inlined Constant CoreCoercion => "Coercion.Coercion".
+Variable CoreCoFunConst : Type. Extract Inlined Constant TyCon => "TyCon.TyCon".
+Variable CoreTyFunConst : Type. Extract Inlined Constant TyCon => "TyCon.TyCon".
+Variable Class_ : Type. Extract Inlined Constant Class_ => "Class.Class".
+Variable classTyCon : Class_ -> TyCon. Extract Inlined Constant classTyCon => "Class.classTyCon".
+Variable tyConToString : TyCon -> string. Extract Inlined Constant tyConToString => "outputableToString".
+Variable dataConToString : CoreDataCon-> string. Extract Inlined Constant dataConToString => "outputableToString".
+Variable tyFunToString : CoreTyFunConst -> string. Extract Inlined Constant tyFunToString => "outputableToString".
+Variable coFunToString : CoreCoFunConst -> string. Extract Inlined Constant coFunToString => "outputableToString".
+Variable natTostring : nat->string. Extract Inlined Constant natTostring => "natTostring".
+Variable CoreIPName : Type -> Type.
+ Extract Constant CoreIPName "’a" => "BasicTypes.IPName".
+ Extraction Inline CoreIPName.