diff --git a/collects/racket/contract/private/provide.rkt b/collects/racket/contract/private/provide.rkt
index 5d44a52b63..578bbe6b83 100644
--- a/collects/racket/contract/private/provide.rkt
+++ b/collects/racket/contract/private/provide.rkt
@@ -636,9 +636,11 @@
        ;; code-for-one-exists-id : syntax -> syntax
        (define (code-for-one-exists-id x x-gen)
          #`(define #,x-gen (new-∃/c '#,x)))
-
+       
        (define (add-exists-binders stx exists-binders)
-         #`(let #,exists-binders #,stx))
+         (if (null? exists-binders)
+             stx
+             #`(let #,exists-binders #,stx)))
        
        (define (add-a-binder id id-gen binders)
          (cons #`[#,id #,id-gen] binders))
@@ -692,25 +694,28 @@
                                          (procedure-arity-includes? id #,(length (syntax->list #'(dom ...)))))]
                                  [_ #f])])
                 (with-syntax ([code
-                               (quasisyntax/loc stx
-                                 (begin
-                                   (define pos-module-source (quote-module-path))
-                                   
-                                   #,@(if no-need-to-check-ctrct?
-                                          (list)
-                                          (list #'(define contract-id 
-                                                    (let ([ex-id ctrct]) ;; let is here to give the right name.
-                                                      (verify-contract 'provide/contract ex-id)))))
-                                   (define-syntax id-rename
-                                     (make-provide/contract-transformer (quote-syntax contract-id)
-                                                                        (quote-syntax id)
-                                                                        (quote-syntax reflect-external-name)
-                                                                        (quote-syntax pos-module-source)))
-                                   
-                                   #,@(if provide?
-                                          (list #`(provide (rename-out [id-rename external-name])))
-                                          null)))])
-                  
+                               (syntax-property
+                                (quasisyntax/loc stx
+                                  (begin
+                                    (define pos-module-source (quote-module-path))
+                                    
+                                    #,@(if no-need-to-check-ctrct?
+                                           (list)
+                                           (list #'(define contract-id 
+                                                     (let ([ex-id ctrct]) ;; let is here to give the right name.
+                                                       (verify-contract 'provide/contract ex-id)))))
+                                    (define-syntax id-rename
+                                      (make-provide/contract-transformer (quote-syntax contract-id)
+                                                                         (quote-syntax id)
+                                                                         (quote-syntax reflect-external-name)
+                                                                         (quote-syntax pos-module-source)))
+                                    
+                                    #,@(if provide?
+                                           (list #`(provide (rename-out [id-rename external-name])))
+                                           null)))
+                                'provide/contract-original-contract
+                                (vector #'external-name #'ctrct))])
+                                
                   (syntax-local-lift-module-end-declaration
                    #`(begin 
                        (unless extra-test
diff --git a/collects/scribblings/reference/contracts.scrbl b/collects/scribblings/reference/contracts.scrbl
index 4fbd04e0cd..eb4124afba 100644
--- a/collects/scribblings/reference/contracts.scrbl
+++ b/collects/scribblings/reference/contracts.scrbl
@@ -748,6 +748,14 @@ The @racket[#:∃] and @racket[#:exists] clauses define new abstract
 contracts. The variables are bound in the remainder of the @racket[provide/contract]
 expression to new contracts that hide the values they accept and
 ensure that the exported functions are treated parametrically.
+
+The implementation of @scheme[provide/contract] attaches uses
+@scheme[syntax-property] to attach properties to the code it generates
+that records the syntax of the contracts in the fully expanded program.
+Specifically, the symbol @scheme['provide/contract-original-contract]
+is bound to vectors of two elements, the exported identifier and a
+syntax object for the expression that produces the contract controlling
+the export.
 }
 
 @defform*/subs[