X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskCoreTypes.v;fp=src%2FHaskCoreTypes.v;h=0fbaeb5b0a432cd24fa7bc4c422d526a96645639;hp=8aa81eeb648513a64ca655e4cec54192776529e7;hb=4ad68fe2894b35c21f2feb7b176d2b0f146ff6d3;hpb=2f503f719116c08f11178e46c3aecfa09d974a82

diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v
index 8aa81ee..0fbaeb5 100644
--- a/src/HaskCoreTypes.v
+++ b/src/HaskCoreTypes.v
@@ -38,6 +38,7 @@ Variable coreCoercionToString  : CoreCoercion -> string.    Extract Inlined Cons
 Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind".
 Variable kindOfCoreType   : CoreType -> Kind.   Extract Inlined Constant kindOfCoreType   => "(coreKindToKind . Coercion.typeKind)".
 Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "(outputableToString . coreViewDeep)".
+Variable setVarType       : CoreVar -> CoreType -> CoreVar. Extract Inlined Constant setVarType       => "Var.setVarType".
 
 (* GHC provides decision procedures for equality on its primitive types; we tell Coq to blindly trust them *)
 Variable coreTyCon_eq         : EqDecider CoreTyCon.       Extract Inlined Constant coreTyCon_eq          => "(==)".