fixed bug related to failure to recertify special-values checking

svn: r3730

collects/stepper/private/annotate.ss

@@ -1069,7 +1069,6 @@
     (define/contract annotate/top-level/acl2
       (syntax? . -> . syntax?)
       (lambda (exp)
-        (>>> exp)
         (syntax-case exp (begin define-values #%app)
           [(begin contract-thingy 
                   (begin body (begin)))
@@ -1146,7 +1145,6 @@
                   #;(error `annotate/module-top-level "unexpected module-top-level expression to annotate: ~a\n" (syntax-object->datum exp))])])))
     
     ; body of local
-    #;(printf "input: ~a\n" exp)
     (let* ([annotated-exp (cond 
                             [(string=? language-level-name "ACL2 Beginner (beta 8)")
                              (annotate/top-level/acl2 main-exp)]

collects/stepper/private/debugger-model.ss

@@ -55,6 +55,8 @@
       
       
       (define (step-through-expression expanded expand-next-expression)
+        (with-output-to-file "/dev/stderr"
+          (printf "about-to-annotate\n"))
         (let* ([annotated (annotate expanded breakpoints breakpoint-origin break)])
           ; (fprintf (current-error-port) "annotated: ~v\n" (syntax-object->datum annotated))
           (let ([expression-result

collects/stepper/private/reconstruct.ss

@@ -217,7 +217,7 @@
                           [(#%app fn . rest)
                            #`fn]
                           [else (error 'find-special-name "couldn't find expanded name for ~a" name)])])      
-      (eval just-the-fn)))
+      (eval (syntax-recertify just-the-fn expanded-application (current-code-inspector) #f))))
 
   ;; these are delayed so that they use the userspace expander.  I'm sure
   ;; there's a more robust & elegant way to do this.