diff --git a/collects/redex/private/gen-trace.rkt b/collects/redex/private/gen-trace.rkt
index 7cb3badf14..81a9483cea 100644
--- a/collects/redex/private/gen-trace.rkt
+++ b/collects/redex/private/gen-trace.rkt
@@ -15,6 +15,7 @@
          "search.rkt"
          "trace-layout.rkt"
          (only-in "pat-unify.rkt"
+                  dq
                   env-eqs
                   env-dqs))
 
@@ -63,10 +64,17 @@
     (when trace
       (show-trace-frame trace))))
 
+;(define-struct gen-trace (tr-loc clause input state bound env) #:prefab)
+#;
+(vector 'info 
+        "generation-log: yes" 
+        (gen-trace '() (clause '(list (list (list))) '() '()'yes) '(list (list (name l_0 (nt l)))) #t 5 (env '#hash() '())) 
+        'generation-log)
+
 (define (format-trace tr)
   (map (match-lambda
              [(vector 'info clause-name
-                      (gen-trace tr-loc clause input state bound env))
+                      (gen-trace tr-loc clause input state bound env) 'generation-log)
               (list (reverse tr-loc) clause-name state input (clause-head-pat clause) bound 0 env)])
            tr))
 
@@ -115,7 +123,7 @@
       [`((,loc ,name ,state ,term ,body ,bound ,depth ,env) ,remaining-traces ...)
        (define atts (attributes name (gensym) (positive? bound) term body (coords #f #f) #f env))
        (loop (insert-tree-atts loc atts tree) remaining-traces)]
-      [else
+      [_
        tree])))
 
 (define (trace-step-loc t-step)
@@ -154,7 +162,7 @@
        (insert-node is node (vector-ref (gen-tree-children tree) i))]
       ['() ;; initial tree (or replacement)
        (set! tree-root node)]
-      [else (error "tree didn't have expected generation pattern" loc tree)]))
+      [_ (error "tree didn't have expected generation pattern" loc tree)]))
   (insert-node full-loc node tree-root)
   tree-root)
 
@@ -170,7 +178,7 @@
       ['() t]
       [`(,i ,is ...)
        (recur (vector-ref (gen-tree-children t) i) is)]
-      [else #f])))
+      [_ #f])))
 
 (define (remove-tree-node loc tree-root)
   (let recur ([t tree-root]
@@ -191,7 +199,7 @@
   (match node
     [(gen-tree loc as cs)
      (set-attributes-focus! as #t)]
-    [else
+    [_
      (void)]))
 
 (define (all-trees trace)
@@ -224,7 +232,7 @@
        (when (> (add1 (length loc)) max-d)
          (set! max-d (add1 (length loc))))
        (loop remaining-traces)]
-      [else max-d])))
+      [_ max-d])))
 
 (define (raw-locs trace)
   (map (match-lambda
@@ -302,7 +310,7 @@
          (for/list ([s subterms]) (prettify-pat s))]
         [`(cstr (,nts ...) ,term)
          `(cstr (,@nts) ,(prettify-pat term))]
-        [else term]))
+        [_ term]))
     
     ;; TODO: "garbage collect" vars,
     ;; treating rule and input as roots
@@ -316,7 +324,7 @@
          (for/list ([s subterms]) (format-pattern s eqs))]
         [`(cstr (,nts ...) ,p)
          `(cstr (,@nts) ,(format-pattern p eqs))]
-        [else p]))
+        [_ p]))
     
     (define/public (update-focus x y-index)
       (defocus)
@@ -330,7 +338,7 @@
         (match t-node
           [(gen-tree loc (attributes p b-f b l l2 (coords x y) f e) cs)
            x]
-          [else +inf.0]))
+          [_ +inf.0]))
       (define closest-node
         (let recur ([t tree]
                     [d (sub1 y-index)])
@@ -352,7 +360,7 @@
         [(gen-tree loc as children)
          (set-attributes-focus! as #t)
          as]
-        [else #f]))
+        [_ #f]))
     
     (define/public (focus-coords)
       (let recur ([t tree])
@@ -382,15 +390,18 @@
                             (match (hash-ref eqs k)
                               [(lvar next) (symbol->string next)]
                               [`(name ,next ,_) (symbol->string next)]
-                              [else " - "]) "\t = "
+                              [_ " - "]) "\t = "
                             (string-replace (pretty-format (format-pattern (hash-ref eqs k) eqs)) "\n" "\n\t   \t   ")))
            "\n")
           "\n\n"
           (string-join
-           (for/list ([dq (in-list (env-dqs e))])
-             (string-append (format "~s" (first dq)) " ≠\n\t"
-                            (format "~s" (second dq))))
-           "\n"))]))
+           (for/list ([a-dq (in-list (env-dqs e))])
+             (match a-dq
+               [(dq ps dq-e)
+                    (string-append "∀ " (format "~s" ps)
+                                   (format "~s" (first dq-e)) " ≠\n\t"
+                                   (format "~s" (second dq-e)))])
+           "\n")))]))
     
     (define/private (defocus)
       (let recur ([t tree])
@@ -410,7 +421,7 @@
          (define atts (attributes name (gensym) (positive? bound) term body (coords #f #f) #t env))
          (set! last-atts atts)
          (set! tree (insert-tree-atts loc atts tree))]
-        [else (error "Trace had incorrect format, failed to update tree")])
+        [_ (error "Trace had incorrect format, failed to update tree")])
       (add-layout-info tree locs->coords))
     
     ))
@@ -482,7 +493,9 @@
       (update-scroll-y y-index))
     
     (define rescale-factor (/ w (t-width)))
-    (define scale-factor (expt rescale-factor (/ 1 (depth))))
+    (define scale-factor (if (= 0 (depth))
+                             1
+                             (expt rescale-factor (/ 1 (depth)))))
     
     (rescale rescale-factor)
     (define canvas (new tree-canvas% [parent this]
@@ -529,7 +542,7 @@
                  (send trace take-step)
                  (update/all-steps)
                  (values #f #f)]
-                [else
+                [_
                  (values #f #f)]))
             (when (and d-x d-y)
               (animate-transition d-x d-y))))
@@ -545,13 +558,13 @@
          (- pos (/ SCROLL-RANGE 20))]
         ['page-down
          (+ pos (/ SCROLL-RANGE 20))]
-        [else pos]))
+        [_ pos]))
     
     (define/private (update-scroll-x x)
       (send canvas set-scroll-pos 'horizontal (+ (* (- x) (/ SCROLL-RANGE (t-width))) 
                                                  (/ SCROLL-RANGE 2))))
     (define/private (update-scroll-y y-index)
-      (send canvas set-scroll-pos 'vertical (max 0 (* (/ y-index (- (depth))) SCROLL-RANGE))))
+      (send canvas set-scroll-pos 'vertical (max 0 (* (/ y-index (- (max 1 (depth)))) SCROLL-RANGE))))
                                           
     (define dc (send canvas get-dc))
     
@@ -663,7 +676,7 @@
     (define/private (animate-transition ∆x ∆y)
       (define scaling (expt scale-factor ∆y))
       (define trans-steps (inexact->exact (ceiling (max (abs (/ (* ∆x 40) (t-width)))
-                                                        (abs (/ (* ∆y 40) (depth)))
+                                                        (if (= 0 (depth)) 0 (abs (/ (* ∆y 40) (depth))))
                                                         1))))
       (define dx (/ ∆x trans-steps))
       (define dy (/ ∆y trans-steps))
diff --git a/collects/redex/private/jdg-gen.rkt b/collects/redex/private/jdg-gen.rkt
index a7bef308d3..5e14bac56e 100644
--- a/collects/redex/private/jdg-gen.rkt
+++ b/collects/redex/private/jdg-gen.rkt
@@ -43,7 +43,7 @@
            (okk (ok))]
           [(? predef-pat? _)
            (okk (ok))]
-          [else p]))))
+          [_ p]))))
   ;; do this first since the term environment (term-e) is needed for the dqs
   (define res-term
     (let recur ([p pat])
@@ -71,7 +71,7 @@
               (and/fail (for/and ([nt (remove nt-pat nts)])
                           ((get-matcher nt) term))
                         term))]
-           [else
+           [_
             (define term (recur pat))
             (and/fail (for/and ([nt nts])
                         ((get-matcher nt) term))
@@ -84,7 +84,7 @@
                       (let ([res (recur p)])
                         (unless (not-failed? res) (fail (unif-fail)))
                         res))))]
-        [else
+        [_
          (make-term p lang)])))
   (and/fail 
    (not-failed? res-term)
@@ -95,7 +95,7 @@
         (or (ok? grook)
             (for/and ([nt nts])
               ((get-matcher nt) grook)))]
-       [else #t]))
+       [_ #t]))
    (check-dqs (remove-empty-dqs (env-dqs full-env)) term-e lang eqs)
    res-term))
 
@@ -145,7 +145,7 @@
           (fail (not-ground))]
          [`(,stuff ...) ;; here it's a fully instanatiated list
           `(,@stuff)]
-         [else
+         [_
           (let-values ([(p bs) (gen-term p lang 2)])
            p)])))))
 
@@ -197,6 +197,6 @@
   (match res
     [(lvar new-id)
      (lookup new-id env)]
-    [else
+    [_
      (values (lvar id) res)]))
 
diff --git a/collects/redex/private/pat-unify.rkt b/collects/redex/private/pat-unify.rkt
index cc00b93c7e..de4d0b5a9a 100644
--- a/collects/redex/private/pat-unify.rkt
+++ b/collects/redex/private/pat-unify.rkt
@@ -115,14 +115,14 @@
                [`(cstr (,nts ...) ,p*)
                 (and (for/and ([n nts]) (n-t? n))
                      (loop p*))]
-               [else #f]))]))))
+               [_ #f]))]))))
 
 (define (pat? p) (pat-or-pat*? #f p))
 (define (pat*? p) (pat-or-pat*? #t p))
 (define pat*-clause-p?s (append (list
-                                 (let ([bound-name? (λ (p) (match p [`(name ,id ,(bound)) #t] [else #f]))])
+                                 (let ([bound-name? (λ (p) (match p [`(name ,id ,(bound)) #t] [_ #f]))])
                                    bound-name?)
-                                 (let ([cstr? (λ (p) (match p [`(cstr (,nts ...) ,pat) #t] [else #f]))])
+                                 (let ([cstr? (λ (p) (match p [`(cstr (,nts ...) ,pat) #t] [_ #f]))])
                                    cstr?))
                                 (extracted-clauses->fns)))
 
@@ -130,7 +130,7 @@
   (match b
     [`(name ,(? var? name) ,(bound))
      #t]
-    [else 
+    [_ 
      #f]))
 
 (define eqs/c
@@ -203,7 +203,7 @@
          [#t 
           (env (hash/mut->imm bn-eqs)
                (env-dqs e))]
-         [else
+         [_
           (env (hash/mut->imm bn-eqs)
                (cons new-dq 
                      (env-dqs e)))])])))
@@ -242,7 +242,7 @@
            `(list ,@(for/list ([p ps]) (recur p)))]
           [`(cstr (,cs ...) p)
            (recur p)]
-          [else
+          [_
            (unless (groundable? p)
              (error resolve-no-nts/pat 
                     "non-groundable pat at internal pattern position: ~s" p))
@@ -255,7 +255,7 @@
     [(? predef-pat? _) #f]
     [`(cstr ,_ ,p)
      (groundable? p)]
-    [else #t]))
+    [_ #t]))
            
                 
 (define (hash/mut->imm h0)
@@ -287,7 +287,7 @@
             (and new-dq
                  (match new-dq
                    [#t (loop ok rest)]
-                   [else (loop (cons new-dq ok) rest)])))])])))
+                   [_ (loop (cons new-dq ok) rest)])))])])))
 
 ;; disunfy* pat* pat* eqs lang -> dq or boolean (dq is a pat*)
 (define (disunify* params u* t* eqs L)
@@ -302,7 +302,7 @@
          (match new-dq
            [`((list) (list))
             #f]
-           [else
+           [_
             (dq new-ps new-dq)])]))))
 
 (define (param-elim params unquantified-dq)             
@@ -359,7 +359,7 @@
                          (hash-set! e (lvar id) (lvar id-new)))]
                       [_ (void)])
                     next]
-                   [else ;; some pat* (res is already bound)
+                   [_ ;; some pat* (res is already bound)
                     (and/fail (not-failed? (unify-update* id b-pat res e L))
                               `(name ,id ,(bound)))])))]
     [`(list ,pats ...)
@@ -413,7 +413,7 @@
                            ,p)]
                    [`(cstr ,nts2 ,new-p)
                     `(cstr ,(merge-ids/sorted nts nts2) ,new-p)]
-                   [else
+                   [_
                     `(cstr ,nts ,res)])))]
     [(_ `(cstr ,nts ,p))
      (unify* `(cstr ,nts ,p) t e L)]
@@ -502,7 +502,7 @@
        [`(name ,next-id ,(bound))
         (hash-set! env (lvar id) (lvar next-id))
         (resolve `(name ,next-id ,(bound)) env)]
-       [else
+       [_
         `(name ,id-rep ,(bound))])]
     [_ pat]))
 
@@ -530,7 +530,7 @@
     ;; or actual values for lvars
     [(? (λ (s) (predef-pat? s)))
      p*]
-    [else
+    [_
      #f]))
 
 ;; occurs* : name (pat* or lvar] -> bool
@@ -553,7 +553,7 @@
          (occurs?* name (hash-ref e (lvar id) (uninstantiated)) e L))]
     [`(cstr ,(lvar _))
      (error 'occurs?* "rogue lvar: ~s\n" p)]
-    [else #f]))
+    [_ #f]))
 
 
 (define (instantiate* id pat e L)
@@ -564,7 +564,7 @@
                (not (occurs?* id (lvar next-id) e L))
                (hash-set! e (lvar id) (lvar next-id))
                `(name ,next-id ,(bound)))]
-    [else
+    [_
      (match pat
        [`(name ,id-2 ,(bound))
         (cond
@@ -579,7 +579,7 @@
                      (unless (ground-pat-eq? id-pat id-2-pat)
                        (hash-set! (new-eqs) (lvar id-2) (lvar id)))
                      `(name ,id ,(bound)))])]
-       [else
+       [_
         (and/fail (not-failed? (unify-update* id id-pat pat e L))
                   `(name ,id ,(bound)))])]))
 
@@ -669,6 +669,6 @@
   (match res
     [(lvar new-id)
      (lookup new-id env)]
-    [else
+    [_
      (values (lvar id) res)]))
 
diff --git a/collects/redex/private/search.rkt b/collects/redex/private/search.rkt
index e396349a84..5a7fcb295b 100644
--- a/collects/redex/private/search.rkt
+++ b/collects/redex/private/search.rkt
@@ -79,7 +79,7 @@
      (match rfs
        [(cons (fail-cont _1 _2 (? (λ (b) (< b 0)) bound)) rest)
         (loop rest)]
-       [else
+       [_
         rfs]))))
 
 (define (shuffle-fails fs)
@@ -93,7 +93,7 @@
   (match fs
     [(list (fail-cont e f b) rest ...)
      (choose-rule e f rest)]
-    [else (values #f fs)]))
+    [_ (values #f fs)]))
 
 (define (choose-rule env fringe fail)
   (cond