diff --git a/cur-doc/cur/scribblings/reflection.scrbl b/cur-doc/cur/scribblings/reflection.scrbl
index 1fae978..839c56d 100644
--- a/cur-doc/cur/scribblings/reflection.scrbl
+++ b/cur-doc/cur/scribblings/reflection.scrbl
@@ -30,52 +30,52 @@ phase 1 in Cur.}
 ]
 }
 
-@defproc[(type-infer/syn [syn syntax?])
+@defproc[(cur-type-infer [syn syntax?])
          (or/c syntax? #f)]{
 Returns the type of the Cur term @racket[syn], or @racket[#f] if no type could be inferred.
 
 @examples[
-(eval:alts (type-infer/syn #'(λ (x : Type) x))
+(eval:alts (cur-type-infer #'(λ (x : Type) x))
            (eval:result @racket[#'(Π (x : (Type 0)) (Type 0))] "" ""))
-(eval:alts (type-infer/syn #'Type)
+(eval:alts (cur-type-infer #'Type)
            (eval:result @racket[#'(Type 1)] "" ""))
 ]
 }
 
-@defproc[(type-check/syn? [syn syntax?])
+@defproc[(cur-type-check? [syn syntax?])
          boolean?]{
 Returns @racket[#t] if the Cur term @racket[syn] is well-typed, or @racket[#f] otherwise.
 
 @examples[
-(eval:alts (type-check/syn? #'(λ (x : Type) x))
+(eval:alts (cur-type-check? #'(λ (x : Type) x))
            (eval:result @racket[#t] "" ""))
-(eval:alts (type-check/syn? #'Type)
+(eval:alts (cur-type-check? #'Type)
            (eval:result @racket[#t] "" ""))
-(eval:alts (type-check/syn? #'x)
+(eval:alts (cur-type-check? #'x)
            (eval:result @racket[#f] "" ""))
 ]
 }
 
-@defproc[(normalize/syn [syn syntax?])
+@defproc[(cur-normalize [syn syntax?])
          syntax?]{
 Runs the Cur term @racket[syn] to a value.
 
 @examples[
-(eval:alts (normalize/syn #'((λ (x : Type) x) Bool))
+(eval:alts (cur-normalize #'((λ (x : Type) x) Bool))
            (eval:result @racket[#'Bool] "" ""))
-(eval:alts (normalize/syn #'(sub1 (s (s z))))
+(eval:alts (cur-normalize #'(sub1 (s (s z))))
            (eval:result @racket[#'(s z)] "" ""))
 ]
 }
 
-@defproc[(step/syn [syn syntax?])
+@defproc[(cur-step [syn syntax?])
          syntax?]{
 Runs the Cur term @racket[syn] for one step.
 
 @examples[
-(eval:alts (step/syn #'((λ (x : Type) x) Bool))
+(eval:alts (cur-step #'((λ (x : Type) x) Bool))
            (eval:result @racket[#'Bool] "" ""))
-(eval:alts (step/syn #'(sub1 (s (s z))))
+(eval:alts (cur-step #'(sub1 (s (s z))))
            (eval:result @racket[#'(((((elim Nat (Type 0))
                                       (λ (x2 : Nat) Nat)) z)
                                     (λ (x2 : Nat) (λ (ih-n2 : Nat) x2)))
diff --git a/cur-doc/cur/scribblings/stdlib/sugar.scrbl b/cur-doc/cur/scribblings/stdlib/sugar.scrbl
index 8ac3e75..e06c21a 100644
--- a/cur-doc/cur/scribblings/stdlib/sugar.scrbl
+++ b/cur-doc/cur/scribblings/stdlib/sugar.scrbl
@@ -169,7 +169,7 @@ Check that expression @racket[e] has type @racket[type], causing a type-error if
 }
 
 @defform[(run syn)]{
-Like @racket[normalize/syn], but is a syntactic form to be used in surface syntax.
+Like @racket[cur-normalize], but is a syntactic form to be used in surface syntax.
 Allows a Cur term to be written by computing part of the term from
 another Cur term.
 
@@ -179,7 +179,7 @@ another Cur term.
 }
 
 @defform[(step syn)]{
-Like @racket[run], but uses @racket[step/syn] to evaluate only one step and prints intermediate
+Like @racket[run], but uses @racket[cur-step] to evaluate only one step and prints intermediate
 results before returning the result of evaluation.
 
 @examples[#:eval curnel-eval
diff --git a/cur-lib/cur/curnel/redex-lang.rkt b/cur-lib/cur/curnel/redex-lang.rkt
index ea67832..dddd82d 100644
--- a/cur-lib/cur/curnel/redex-lang.rkt
+++ b/cur-lib/cur/curnel/redex-lang.rkt
@@ -60,10 +60,10 @@
    (all-from-out racket/syntax)
     cur->datum
     cur-expand
-    type-infer/syn
-    type-check/syn?
-    normalize/syn
-    step/syn
+    cur-type-infer
+    cur-type-check?
+    cur-normalize
+    cur-step
     cur-equal?))
 
 (begin-for-syntax
@@ -224,12 +224,12 @@
 
   ;; Reflection tools
 
-  (define (normalize/syn syn)
+  (define (cur-normalize syn)
     (datum->cur
       syn
       (eval-cur syn)))
 
-  (define (step/syn syn)
+  (define (cur-step syn)
     (datum->cur
       syn
       (term (step ,(delta) ,(subst-bindings (cur->datum syn))))))
@@ -239,14 +239,14 @@
     (and (judgment-holds (equivalent ,(delta) ,(eval-cur e1) ,(eval-cur e2))) #t))
 
   ;; TODO: Document local-env
-  (define (type-infer/syn syn #:local-env [env '()])
+  (define (cur-type-infer syn #:local-env [env '()])
     (parameterize ([gamma (for/fold ([gamma (gamma)])
                                     ([(x t) (in-dict env)])
                             (extend-Γ/syn (thunk gamma) x t))])
       (let ([t (type-infer/term (eval-cur syn))])
         (and t (datum->cur syn t)))))
 
-  (define (type-check/syn? syn type)
+  (define (cur-type-check? syn type)
     (type-check/term? (eval-cur syn) (eval-cur type)))
 
   ;; Takes a Cur term syn and an arbitrary number of identifiers ls. The cur term is
diff --git a/cur-lib/cur/olly.rkt b/cur-lib/cur/olly.rkt
index bb064c2..186df48 100644
--- a/cur-lib/cur/olly.rkt
+++ b/cur-lib/cur/olly.rkt
@@ -32,7 +32,7 @@
     (coq-defns (format "~a~a~n" (coq-defns) str)))
 
   (define (constructor-args syn)
-    (syntax-parse (type-infer/syn syn)
+    (syntax-parse (cur-type-infer syn)
       #:datum-literals (Π :)
       [(Π (x:id : t) body)
        (cons #'x (constructor-args #'body))]
diff --git a/cur-lib/cur/stdlib/maybe.rkt b/cur-lib/cur/stdlib/maybe.rkt
index 6f70d48..9625d77 100644
--- a/cur-lib/cur/stdlib/maybe.rkt
+++ b/cur-lib/cur/stdlib/maybe.rkt
@@ -9,5 +9,5 @@
 (define-syntax (some/i syn)
   (syntax-case syn ()
    [(_ a)
-    (let ([a-ty (type-infer/syn #'a)])
+    (let ([a-ty (cur-type-infer #'a)])
       #`(some #,a-ty a))]))
diff --git a/cur-lib/cur/stdlib/prop.rkt b/cur-lib/cur/stdlib/prop.rkt
index d70b69f..3030ad7 100644
--- a/cur-lib/cur/stdlib/prop.rkt
+++ b/cur-lib/cur/stdlib/prop.rkt
@@ -31,8 +31,8 @@
 (define-syntax (conj/i syn)
   (syntax-case syn ()
     [(_ a b)
-     (let ([a-type (type-infer/syn #'a)]
-           [b-type (type-infer/syn #'b)])
+     (let ([a-type (cur-type-infer #'a)]
+           [b-type (cur-type-infer #'b)])
        #`(conj #,a-type #,b-type a b))]))
 
 (define thm:and-is-symmetric
diff --git a/cur-lib/cur/stdlib/sugar.rkt b/cur-lib/cur/stdlib/sugar.rkt
index dc42302..958362d 100644
--- a/cur-lib/cur/stdlib/sugar.rkt
+++ b/cur-lib/cur/stdlib/sugar.rkt
@@ -162,7 +162,7 @@
      #:attr types
      ;; TODO: Detect failure, report error/suggestions
      (for/list ([e (attribute indices)])
-       (or (type-infer/syn e)
+       (or (cur-type-infer e)
            (raise-syntax-error
             'match
             (format
@@ -183,7 +183,7 @@
      (lambda (return)
        ;; NB: unhygenic
        ;; Normalize at compile-time, for efficiency at run-time
-       (normalize/syn
+       (cur-normalize
         #`((lambda
               ;; TODO: utteraly fragile; relines on the indices being referred to by name, not computed
               ;; works only for simple type familes and simply matches on them
@@ -244,7 +244,7 @@
        (define/syntax-parse type:inductive-type-declaration (cur-expand type-syn))
        (let ([ih-name (quasisyntax/loc src #,(format-id name-syn "ih-~a" name-syn))]
              ;; Normalize at compile-time, for efficiency at run-time
-             [ih-type (normalize/syn #`(#,motive #,@(attribute type.indices) #,name-syn))])
+             [ih-type (cur-normalize #`(#,motive #,@(attribute type.indices) #,name-syn))])
          (dict-set! ih-dict (syntax->datum name-syn) ih-name)
          (append decls (list #`(#,ih-name : #,ih-type)))))))
 
@@ -256,7 +256,7 @@
      (or maybe-return-type
          ;; Ignore errors when trying to infer this type; other attempt might succeed
          (with-handlers ([values (lambda _ #f)])
-           (type-infer/syn #:local-env (attribute p.local-env) #'b)))))
+           (cur-type-infer #:local-env (attribute p.local-env) #'b)))))
 
   (define-syntax-class (match-clause D motive)
     (pattern
@@ -292,7 +292,7 @@
         (~optional
          (~seq #:in ~! t)
          #:defaults
-         ([t (or (type-infer/syn #'d)
+         ([t (or (cur-type-infer #'d)
                  (raise-syntax-error
                   'match
                   "Could not infer discrimnant's type. Try using #:in to declare it."
@@ -318,7 +318,7 @@
        (elim
         D.inductive-name
         #,(or
-           (type-infer/syn (attribute return-type))
+           (cur-type-infer (attribute return-type))
            (raise-syntax-error
             'match
             "Could not infer type of motive. Sorry, you'll have to use elim."
@@ -337,14 +337,14 @@
       #:attr type (cond
                     [(attribute t)
                      ;; TODO: Code duplication in ::
-                     (unless (type-check/syn? #'e #'t)
+                     (unless (cur-type-check? #'e #'t)
                        (raise-syntax-error
                          'let
                          (format "Term ~a does not have expected type ~a. Inferred type was ~a"
-                                 (cur->datum #'e) (cur->datum #'t) (cur->datum (type-infer/syn #'e)))
+                                 (cur->datum #'e) (cur->datum #'t) (cur->datum (cur-type-infer #'e)))
                          #'e (quasisyntax/loc #'x (x e))))
                      #'t]
-                    [(type-infer/syn #'e)]
+                    [(cur-type-infer #'e)]
                     [else
                       (raise-syntax-error
                         'let
@@ -362,22 +362,22 @@
     [(_ pf t)
      (begin
        ;; TODO: Code duplication in let-clause pattern
-       (unless (type-check/syn? #'pf #'t)
+       (unless (cur-type-check? #'pf #'t)
          (raise-syntax-error
            '::
            (format "Term ~a does not have expected type ~a. Inferred type was ~a"
-                   (cur->datum #'pf) (cur->datum #'t) (cur->datum (type-infer/syn #'pf)))
+                   (cur->datum #'pf) (cur->datum #'t) (cur->datum (cur-type-infer #'pf)))
            syn))
        #'(void))]))
 
 (define-syntax (run syn)
   (syntax-case syn ()
-    [(_ expr) (normalize/syn #'expr)]))
+    [(_ expr) (cur-normalize #'expr)]))
 
 (define-syntax (step syn)
   (syntax-case syn ()
     [(_ expr)
-     (let ([t (step/syn #'expr)])
+     (let ([t (cur-step #'expr)])
        (displayln (cur->datum t))
        t)]))
 
@@ -393,6 +393,6 @@
   (syntax-case syn ()
     [(_ term)
      (begin
-       (printf "\"~a\" has type \"~a\"~n" (syntax->datum #'term) (syntax->datum (type-infer/syn #'term)))
+       (printf "\"~a\" has type \"~a\"~n" (syntax->datum #'term) (syntax->datum (cur-type-infer #'term)))
        ;; Void is undocumented and a hack, but sort of works
        #'(void))]))
diff --git a/cur-lib/cur/stdlib/tactics/base.rkt b/cur-lib/cur/stdlib/tactics/base.rkt
index c504222..ce2ef26 100644
--- a/cur-lib/cur/stdlib/tactics/base.rkt
+++ b/cur-lib/cur/stdlib/tactics/base.rkt
@@ -220,7 +220,7 @@
            [pf (proof-state-proof ps)])
       (unless (proof-state-proof-complete? ps)
         (raise-syntax-error 'qed "Proof contains holes" (pf (current-hole-pretty-symbol))))
-      (unless (type-check/syn? pf t)
+      (unless (cur-type-check? pf t)
         (raise-syntax-error 'qed "Invalid proof" pf t))
       pf)))
 
diff --git a/cur-lib/cur/stdlib/typeclass.rkt b/cur-lib/cur/stdlib/typeclass.rkt
index 3c26dc3..dc24209 100644
--- a/cur-lib/cur/stdlib/typeclass.rkt
+++ b/cur-lib/cur/stdlib/typeclass.rkt
@@ -38,7 +38,7 @@
               #`(define-syntax (#,name syn)
                   (syntax-case syn ()
                     [(_ arg args (... ...))
-                     #`(#,(format-id syn "~a-~a" '#,name (type-infer/syn #'arg))
+                     #`(#,(format-id syn "~a-~a" '#,name (cur-type-infer #'arg))
                         arg
                         args (... ...))]))))]))
 
@@ -57,7 +57,7 @@
      #`(begin
          #,@(for/list ([def (syntax->list #'(defs ...))])
               (let-values ([(name body) (process-def def)])
-                (unless (type-check/syn?
+                (unless (cur-type-check?
                           body
                           #`(#,(dict-ref
                                  (dict-ref typeclasses (syntax->datum #'class))