diff --git a/collects/typed-scheme/env/type-name-env.ss b/collects/typed-scheme/env/type-name-env.ss
index 7c41a3de..69b98825 100644
--- a/collects/typed-scheme/env/type-name-env.ss
+++ b/collects/typed-scheme/env/type-name-env.ss
@@ -46,6 +46,6 @@
 (define (type-name-env-map f)
   (module-identifier-mapping-map the-mapping f))
 
-(define (add-alias from to)  
+(define (add-alias from to)
   (when (lookup-type-name to (lambda () #f))
     (register-resolved-type-alias from (make-Name to))))
\ No newline at end of file
diff --git a/collects/typed-scheme/infer/infer-unit.ss b/collects/typed-scheme/infer/infer-unit.ss
index 18ff9b65..20bbf1f2 100644
--- a/collects/typed-scheme/infer/infer-unit.ss
+++ b/collects/typed-scheme/infer/infer-unit.ss
@@ -242,10 +242,10 @@
             (S T)
           [(a a) empty]
           [(_ (Univ:)) empty]
-          
+
           [((Refinement: S _ _) T)
            (cg S T)]
-          
+
           [((F: (? (lambda (e) (memq e X)) v)) S)
            (when (match S
                    [(F: v*)
@@ -260,7 +260,7 @@
                    [_ #f])
              (fail! S T))
            (singleton (var-promote S V) v Univ)]
-          
+
           ;; two unions with the same number of elements, so we just try to unify them pairwise
           #;[((Union: l1) (Union: l2))
              (=> unmatch)
diff --git a/collects/typed-scheme/ts-reference.scrbl b/collects/typed-scheme/ts-reference.scrbl
index d2911b68..14e73bdb 100644
--- a/collects/typed-scheme/ts-reference.scrbl
+++ b/collects/typed-scheme/ts-reference.scrbl
@@ -40,7 +40,7 @@
 @defidform[Namespace]
 @defidform[EOF]
 @defidform[Char])]{
-These types represent primitive Scheme data.}
+These types represent primitive Scheme data.  Note that @scheme[Integer] represents exact integers.}
 
 @defidform[Any]{Any Scheme value. All other types are subtypes of @scheme[Any].}
 
diff --git a/collects/typed-scheme/types/printer.ss b/collects/typed-scheme/types/printer.ss
index 7bef89b3..6d919bf6 100644
--- a/collects/typed-scheme/types/printer.ss
+++ b/collects/typed-scheme/types/printer.ss
@@ -181,6 +181,8 @@
     [(Result: t (LFilterSet: (list) (list)) (LEmpty:)) (fp "~a" t)]
     [(Result: t fs (LEmpty:)) (fp "(~a : ~a)" t fs)]
     [(Result: t fs lo) (fp "(~a : ~a : ~a)" t fs lo)]
+    [(Refinement: parent p? _)
+     (fp "(Refinement ~a ~a)" parent (syntax-e p?))]
     [else (fp "Unknown Type: ~a" (struct->vector c))]
     ))
 
diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss
index 20570e2b..14f2ab3c 100644
--- a/collects/typed-scheme/types/subtype.ss
+++ b/collects/typed-scheme/types/subtype.ss
@@ -226,6 +226,8 @@
 		       (unmatch))
 					;(printf "Poly: ~n~a ~n~a~n" b1 (subst-all (map list ms (map make-F ns)) b2))
 	       (subtype* A0 b1 (subst-all (map list ms (map make-F ns)) b2))]
+	      [(list (Refinement: par _ _) t)
+               (subtype* A0 par t)]
 	      ;; use unification to see if we can use the polytype here
 	      [(list (Poly: vs b) s)
 	       (=> unmatch)
diff --git a/collects/typed-scheme/utils/require-contract.ss b/collects/typed-scheme/utils/require-contract.ss
index 73570ff2..eb9bbff4 100644
--- a/collects/typed-scheme/utils/require-contract.ss
+++ b/collects/typed-scheme/utils/require-contract.ss
@@ -1,6 +1,9 @@
 #lang scheme/base
 
-(require scheme/contract (for-syntax scheme/base syntax/kerncase))
+(require scheme/contract (for-syntax scheme/base syntax/kerncase 
+                                     "../utils/tc-utils.ss"
+                                     (prefix-in tr: "../private/typed-renaming.ss")))
+
 (provide require/contract define-ignored)
 
 (define-syntax (define-ignored stx)
@@ -20,12 +23,30 @@
                                           'inferred-name
                                           (syntax-e #'name)))])]))
 
+
+(define-syntax (get-alternate stx)
+  (syntax-case stx ()
+    [(_ id)
+     (tr:get-alternate #'id)]))
+
 (define-syntax (require/contract stx)
   (syntax-case stx ()
     [(require/contract nm cnt lib)
      (identifier? #'nm)
-     #`(begin (require (only-in lib [nm tmp]))     
-              (define-ignored nm (contract cnt tmp '(interface for #,(syntax->datum #'nm)) 'never-happen (quote-syntax nm))))]
+     (begin       
+       #`(begin (require (only-in lib [nm tmp]))     
+                (define-ignored nm 
+                  (contract cnt 
+                            (get-alternate tmp)
+                            '(interface for #,(syntax->datum #'nm))
+                            'never-happen
+                            (quote-syntax nm)))))]
     [(require/contract (orig-nm nm) cnt lib)     
-     #`(begin (require (only-in lib [orig-nm tmp]))
-              (define-ignored nm (contract cnt tmp '#,(syntax->datum #'nm) 'never-happen (quote-syntax nm))))]))
+     (begin 
+       #`(begin (require (only-in lib [orig-nm tmp]))
+                (define-ignored nm 
+                  (contract cnt 
+                            (get-alternate tmp) 
+                            '#,(syntax->datum #'nm)
+                            'never-happen
+                            (quote-syntax nm)))))]))