Work on comments

Fix typos, add some documentation and erase irrelevant comments

Author: ProgMiner

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

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; *)

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

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

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

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