diff --git a/OCanren-ppx.opam b/OCanren-ppx.opam
index f5f0c18de..f22e69077 100644
--- a/OCanren-ppx.opam
+++ b/OCanren-ppx.opam
@@ -33,7 +33,7 @@ homepage: "https://github.com/PLTools/OCanren"
 bug-reports: "https://github.com/PLTools/OCanren/issues"
 depends: [
   "dune" {>= "2.9"}
-  "ocaml" {>= "4.10"}
+  "ocaml" {>= "4.14.2"}
   "dune-configurator"
   "ppxlib" {>= "0.26.0" & <= "0.28.0"}
   "ppx_inline_test_nobase"
diff --git a/OCanren.opam b/OCanren.opam
index 26731cd22..24c70a74c 100644
--- a/OCanren.opam
+++ b/OCanren.opam
@@ -24,7 +24,7 @@ homepage: "https://github.com/PLTools/OCanren"
 bug-reports: "https://github.com/PLTools/OCanren/issues"
 depends: [
   "dune" {>= "2.9"}
-  "ocaml" {>= "4.10"}
+  "ocaml" {>= "4.14.2"}
   "dune-configurator"
   "ocamlfind"
   "camlp5"
diff --git a/dune-project b/dune-project
index 9978768f7..4506d7282 100644
--- a/dune-project
+++ b/dune-project
@@ -19,7 +19,7 @@
   "The family of miniKanren derivatives has many implementations. This\none is typed embedding to OCaml. The original implementation for\nthis is in scheme and can be found at https://github.com/michaelballantyne/faster-miniKanren .\n\nFeatures:\n1) disequality constraints\n2) relational standard library: lists, nats\n")
  (depends
   (ocaml
-   (>= 4.10))
+   (>= 4.14.2))
   dune-configurator
   ocamlfind
   camlp5
@@ -53,7 +53,7 @@
   "PPX rewriters for writing relational programs more conveniently.\n\n1) `ppx_fresh` -- a clone of original miniKanren syntax\n\n  fresh (x...) goal\n\nexpands into\n\n  Fresh.numeral (fun x ... -> goal)\n\n2) `ppx_distrib` for easier generation of type-safe wrappers: distrib functor, etc...\n\n  [%%distrib\n    type t = fully_abstract_typee\n    type ground = ...\n  ]\n\n3) `ppx_repr` for test. Expands `REPR(expr)` to `(string_of_expr expr, expr)`\n")
  (depends
   (ocaml
-   (>= 4.10))
+   (>= 4.14.2))
   dune-configurator
   (ppxlib
    (and
diff --git a/src/core/Core.ml b/src/core/Core.ml
index 93dbf6dd0..99e6bbaac 100644
--- a/src/core/Core.ml
+++ b/src/core/Core.ml
@@ -154,7 +154,6 @@ module Prunes : sig
   type t
 
   val empty   : t
-  (* Returns false when constraints are violated *)
   val recheck : t -> Env.t -> Subst.t -> rez
   val check_last : t -> Env.t -> Subst.t -> rez
   val extend  : t -> Term.VarTbl.key -> ('a, 'b) reifier -> 'b cond -> t
diff --git a/src/core/Disequality.ml b/src/core/Disequality.ml
index ae3c28e3e..3b5c481e0 100644
--- a/src/core/Disequality.ml
+++ b/src/core/Disequality.ml
@@ -178,8 +178,8 @@ module Disjunct :
           raise Disequality_fulfilled
       | Refined delta  -> (
           (* When leading terms are reified into something new, we still need to
-             do whole unification, beacuse other pairs may need walking ---
-             (we postponed walking, so som einformation may be lost.)
+             do whole unification, because other pairs may need walking ---
+             (we postponed walking, so some information may be lost.)
              See issue #173
           *)
           (* log "Refined into: %a" (Format.pp_print_list Subst.Binding.pp) delta; *)
diff --git a/src/core/Logic.ml b/src/core/Logic.ml
index 4f2fde452..fa3ec3e5f 100644
--- a/src/core/Logic.ml
+++ b/src/core/Logic.ml
@@ -87,10 +87,6 @@ module Reifier = struct
         let i, cs = Term.Var.reify (reify env) v in
         Var (i, cs)
 
-  (* can be implemented more efficiently,
-    * without allocation of `'a logic`,
-    * but for demonstration purposes this implementation is okay
-    *)
   let prj_exn : ('a ilogic, 'a) t =
     fun env t ->
       match Term.var t with
diff --git a/src/core/Logic.mli b/src/core/Logic.mli
index f3031a693..60f4b66cd 100644
--- a/src/core/Logic.mli
+++ b/src/core/Logic.mli
@@ -62,7 +62,9 @@ module Reifier : sig
   *)
   val prj_exn : ('a ilogic, 'a) t
 
-  (* TODO(Kakadu): document this *)
+  (** [prj onvar] Projects implicit logic into the underlying type,
+   *  handling logic variables with [onvar]
+   *)
   val prj : (int -> 'a) -> ('a ilogic, 'a) t
 
   (* Interesting part --- we can apply a reifier to a value dipped into `State.t` comonad *)
@@ -82,7 +84,7 @@ module Reifier : sig
   (** Fixpoint for reifier. *)
   val fix: ( ('a, 'b) t as 'c -> 'c) -> 'c
 
-  (** And uxiliary function to make reifiers generated by generic programming point-free. *)
+  (** An auxiliary function to make reifiers generated by generic programming point-free. *)
   val rework : fv:('a Env.m -> 'b Env.m)
       -> ('a logic Env.m -> 'b logic Env.m)
       -> 'a logic Env.m
diff --git a/src/core/Subst.mli b/src/core/Subst.mli
index a06d8e219..62d2257cd 100644
--- a/src/core/Subst.mli
+++ b/src/core/Subst.mli
@@ -89,6 +89,7 @@ module Answer :
     val subsumed : Env.t -> t -> t -> bool
   end
 
+(* see [apply] *)
 val reify : Env.t -> t -> 'a -> Answer.t
 
 IFDEF STATS THEN
diff --git a/tester/tester.mli b/tester/tester.mli
index c28810580..b87cf888a 100644
--- a/tester/tester.mli
+++ b/tester/tester.mli
@@ -1,7 +1,7 @@
 (** {1 Main}   *)
 
-(** In this module you can find convenience functions to speedup your introduction to OCanre.
-    In realy projects, more likely you will need more low-level interface like {!OCanren.run}. *)
+(** In this module you can find convenience functions to speedup your introduction to OCanren.
+    In real projects, more likely you will need more low-level interface like {!OCanren.run}. *)
 
 (**
   The call [run_r reifier to_string count num num_handler ("description", goal)] should be used