diff --git a/coq-extraction.rkt b/coq-extraction.rkt
deleted file mode 100644
index 1e20712..0000000
--- a/coq-extraction.rkt
+++ /dev/null
@@ -1,72 +0,0 @@
-#lang s-exp "cur-redex.rkt"
-
-(begin-for-syntax
-  (define orig-insp (variable-reference->module-declaration-inspector
-    (#%variable-reference)))
-
-  (define (disarm syn) (syntax-disarm syn orig-insp))
-
-  ;; TODO: Pull expand, perhaps list of literals, into a library.
-  (define (expand syn)
-    (disarm (local-expand syn 'expression (syntax-e #'(lambda forall data case fix Type #%app #%top)))))
-
-  (define (output-coq syn)
-    (syntax-parse (expand syn)
-       [((~literal lambda) ~! (x:id (~datum :) t) body:expr)
-        (format "(fun ~a : ~a => ~a)" (syntax-e #'x) (output-coq #'t)
-                (output-coq #'body))]
-       [((~literal forall) ~! (x:id (~datum :) t) body:expr)
-        (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (output-coq #'t)
-                (output-coq #'body))]
-       [((~literal data) ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)
-        (format "Inductive ~a : ~a :=~n~a."
-                (syntax-e #'n)
-                (output-coq #'t)
-                (string-trim
-                  (for/fold ([strs ""])
-                            ([clause (syntax->list #'((x* : t*) ...))])
-                    (syntax-parse clause
-                      [(x (~datum :) t)
-                       (format "~a~a : ~a~n| " strs (syntax-e #'x)
-                               (output-coq #'t))]))
-                  #px"\\s\\| $"
-                  #:left? #f))]
-       ;; TODO: Add "case". Will be slightly tricky since the syntax is
-       ;; quite different from Coq.
-       [(e1 e* ...)
-        (format "(~a~a)" (output-coq #'e1)
-          (for/fold ([strs ""])
-                    ([arg (syntax->list #'(e* ...))])
-            (format "~a ~a" strs (output-coq arg))))]
-       [e:id (format "~a" (syntax->datum #'e))])))
-
-(define-syntax (generate-coq syn)
-  (syntax-parse syn
-    [(_ (~optional (~seq #:file file)) body:expr)
-     (parameterize ([current-output-port (if (attribute file)
-                                             (syntax->datum #'file)
-                                             (current-output-port))])
-       (displayln (output-coq #'body))
-       #'Type)]))
-
-(module+ test
-  (require "sugar.rkt" "pltools.rkt")
-  (begin-for-syntax
-    (require rackunit)
-    (check-equal?
-      (format "Inductive nat : Type :=~nz : nat.")
-      (output-coq #'(data nat : Type (z : nat))))
-    (check-regexp-match
-      "(forall .+ : Type, Type)"
-      (output-coq #'(-> Type Type)))
-    ;; TODO: Not sure why these tests are failing.
-    (let ([t (output-coq #'(define-relation (meow gamma term type)
-                             [(g : gamma) (e : term) (t : type)
-                              --------------- T-Bla
-                              (meow g e t)]))])
-      (check-regexp-match
-        "Inductive meow : (forall temp. : gamma, (forall temp. : term, (forall temp. : type, Type))) :="
-        (first (string-split t "\n")))
-      (check-regexp-match
-        "T-Bla : (forall g : gamma, (forall e : term, (forall t : type, (meow g e t))))\\."
-        (second (string-split t "\n"))))))
diff --git a/pltools.rkt b/oll.rkt
similarity index 67%
rename from pltools.rkt
rename to oll.rkt
index ae5b44c..0e5ed9f 100644
--- a/pltools.rkt
+++ b/oll.rkt
@@ -1,5 +1,7 @@
 #lang s-exp "cur-redex.rkt"
+;; OLL: The OTT-Like Library
 (require "sugar.rkt" "nat.rkt")
+
 ;; TODO: Can't export var, avar because technically these aren't
 ;; defined....
 ;; REALLY NEED TO FIX THAT
@@ -163,3 +165,74 @@
     (stlc-val-->-stlc-term : (-> stlc-val stlc-term))
     (stlc-term2151 : (->* stlc-term stlc-term stlc-term))
     (stlc-lambda : (->* var stlc-type stlc-term stlc-term))))
+
+(begin-for-syntax
+  (define orig-insp (variable-reference->module-declaration-inspector
+    (#%variable-reference)))
+
+  (define (disarm syn) (syntax-disarm syn orig-insp))
+
+  ;; TODO: Pull expand, perhaps list of literals, into a library.
+  (define (expand syn)
+    (disarm (local-expand syn 'expression (syntax-e #'(lambda forall data case fix Type #%app #%top)))))
+
+  (define (output-coq syn)
+    (syntax-parse (expand syn)
+       [((~literal lambda) ~! (x:id (~datum :) t) body:expr)
+        (format "(fun ~a : ~a => ~a)" (syntax-e #'x) (output-coq #'t)
+                (output-coq #'body))]
+       [((~literal forall) ~! (x:id (~datum :) t) body:expr)
+        (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (output-coq #'t)
+                (output-coq #'body))]
+       [((~literal data) ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)
+        (format "Inductive ~a : ~a :=~n~a."
+                (syntax-e #'n)
+                (output-coq #'t)
+                (string-trim
+                  (for/fold ([strs ""])
+                            ([clause (syntax->list #'((x* : t*) ...))])
+                    (syntax-parse clause
+                      [(x (~datum :) t)
+                       (format "~a~a : ~a~n| " strs (syntax-e #'x)
+                               (output-coq #'t))]))
+                  #px"\\s\\| $"
+                  #:left? #f))]
+       ;; TODO: Add "case". Will be slightly tricky since the syntax is
+       ;; quite different from Coq.
+       [(e1 e* ...)
+        (format "(~a~a)" (output-coq #'e1)
+          (for/fold ([strs ""])
+                    ([arg (syntax->list #'(e* ...))])
+            (format "~a ~a" strs (output-coq arg))))]
+       [e:id (format "~a" (syntax->datum #'e))])))
+
+(define-syntax (generate-coq syn)
+  (syntax-parse syn
+    [(_ (~optional (~seq #:file file)) body:expr)
+     (parameterize ([current-output-port (if (attribute file)
+                                             (syntax->datum #'file)
+                                             (current-output-port))])
+       (displayln (output-coq #'body))
+       #'Type)]))
+
+(module+ test
+  (require "sugar.rkt")
+  (begin-for-syntax
+    (require rackunit)
+    (check-equal?
+      (format "Inductive nat : Type :=~nz : nat.")
+      (output-coq #'(data nat : Type (z : nat))))
+    (check-regexp-match
+      "(forall .+ : Type, Type)"
+      (output-coq #'(-> Type Type)))
+    ;; TODO: Not sure why these tests are failing.
+    (let ([t (output-coq #'(define-relation (meow gamma term type)
+                             [(g : gamma) (e : term) (t : type)
+                              --------------- T-Bla
+                              (meow g e t)]))])
+      (check-regexp-match
+        "Inductive meow : (forall temp. : gamma, (forall temp. : term, (forall temp. : type, Type))) :="
+        (first (string-split t "\n")))
+      (check-regexp-match
+        "T-Bla : (forall g : gamma, (forall e : term, (forall t : type, (meow g e t))))\\."
+        (second (string-split t "\n"))))))
diff --git a/proofs-for-free-v2.rkt b/proofs-for-free-v2.rkt
index 604bcea..6973052 100644
--- a/proofs-for-free-v2.rkt
+++ b/proofs-for-free-v2.rkt
@@ -1,4 +1,5 @@
 #lang s-exp "cur-redex.rkt"
+;; Ignore this file.
 (require rackunit racket/trace (for-syntax racket/syntax))
 
 ;; TODO: Move to standard library