diff --git a/NominalAngluin.cabal b/NominalAngluin.cabal
index e0783ce..1e74be8 100644
--- a/NominalAngluin.cabal
+++ b/NominalAngluin.cabal
@@ -7,8 +7,8 @@ version:             0.1.0.0
 -- description:         
 -- license:             
 license-file:        LICENSE
-author:              Joshua Moerman
-maintainer:          lakseru@gmail.com
+author:              Anonymous
+-- maintainer:          
 -- copyright:           
 -- category:            
 build-type:          Simple
diff --git a/src/Angluin.hs b/src/Angluin.hs
index 0e107a3..b9de749 100644
--- a/src/Angluin.hs
+++ b/src/Angluin.hs
@@ -54,7 +54,6 @@ useCounterExampleAngluin teacher state@State{..} ces =
     addRows teacher ds state
 
 -- This is the variant by Maler and Pnueli
--- I used to think it waw Rivest and Schapire, but they add less columns
 useCounterExampleMP :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i
 useCounterExampleMP teacher state@State{..} ces =
     trace ("Using ce: " ++ show ces) $
@@ -79,9 +78,9 @@ learnAngluinRows teacher = learn makeCompleteAngluin useCounterExampleAngluin co
 -- Below are some variations of the above functions with different
 -- performance characteristics.
 
--- Joshua's slower version
-consistencyTestJ :: NominalType i => State i -> TestResult i
-consistencyTestJ State{..} = case solve (isEmpty defect) of
+-- Some coauthor's slower version
+consistencyTest2 :: NominalType i => State i -> TestResult i
+consistencyTest2 State{..} = case solve (isEmpty defect) of
     Just True  -> Succes
     Just False -> trace "Not consistent" $ Failed empty columns
     where
@@ -95,9 +94,9 @@ consistencyTestJ State{..} = case solve (isEmpty defect) of
                  ) ss ss aa
         columns = sum $ map (\((s1,s2,a),es) -> map (a:) es) defect
 
--- Bartek's faster version
-consistencyTestB :: NominalType i => State i -> TestResult i
-consistencyTestB State{..} = case solve (isEmpty defect) of
+-- Some coauthor's faster version
+consistencyTest3 :: NominalType i => State i -> TestResult i
+consistencyTest3 State{..} = case solve (isEmpty defect) of
     Just True  -> Succes
     Just False -> trace "Not consistent" $ Failed empty columns
     where
diff --git a/src/Bollig.hs b/src/Bollig.hs
index d0bf85c..e74b8fd 100644
--- a/src/Bollig.hs
+++ b/src/Bollig.hs
@@ -30,7 +30,6 @@ sublang r1 r2 = forAll fromBool $ pairsWithFilter (\(i1, f1) (i2, f2) -> maybeIf
 sublangs :: NominalType i => BRow i -> Set (BRow i) -> Set (BRow i)
 sublangs r set = filter (\r2 -> r2 `sublang` r) set
 
--- Infinitary version ?
 rfsaClosednessTest2 :: LearnableAlphabet i => State i -> TestResult i
 rfsaClosednessTest2 State{..} = case solve (isEmpty defect) of
     Just True  -> Succes
diff --git a/src/NLStar.hs b/src/NLStar.hs
index 4af1ed8..293806b 100644
--- a/src/NLStar.hs
+++ b/src/NLStar.hs
@@ -25,7 +25,10 @@ import           Prelude          hiding (and, curry, filter, lookup, map, not,
    Sounds a bit crazy, but the teacher kind of takes care of that. Of course
    I do not know whether this will terminate. But it's nice to experiment with.
    Also I do not 'minimize' the NFA by taking only prime rows. Saves a lot of
-   checking but makes the result not minimal (whatever that would mean).
+   checking but makes the result not minimal (whatever that would mean). It
+   is quite fast, however ;-).
+
+   THIS IS NOT USED IN THE PAPER.
 -}
 
 -- We can determine its completeness with the following
diff --git a/src/ObservationTable.hs b/src/ObservationTable.hs
index 24e0b3b..7b6a795 100644
--- a/src/ObservationTable.hs
+++ b/src/ObservationTable.hs
@@ -29,7 +29,6 @@ apply f a1 = mapFilter (\(a2, b) -> maybeIf (eq a1 a2) b) f
 
 -- Returns the subset (of the domain) which exhibits
 -- different return values for the two functions
--- I am not sure about its correctness...
 discrepancy :: (NominalType a, NominalType b) => Fun a b -> Fun a b -> Set a
 discrepancy f1 f2 =
     pairsWithFilter (
diff --git a/src/Teacher.hs b/src/Teacher.hs
index a875fe2..d8f6311 100644
--- a/src/Teacher.hs
+++ b/src/Teacher.hs
@@ -27,9 +27,12 @@ import           Text.Read               (readMaybe)
 
 -- Abstract teacher type (inside the NLambda library, ideally one would like
 -- an external interface, with Bool as output instead of Formula for instance)
+-- For now we do actually implement an external teacher, but it is rather hacky.
 data Teacher i = Teacher
     -- Given a sequence, check whether it is in the language
-    -- Assumed to be equivariant
+    -- Assumed to be equivariant.
+    -- We slightly change the type to support counting the number of orbits.
+    -- All teacher (except the counting one) implement membership :: [i] -> Formula
     { membership :: Set [i] -> Set ([i], Formula)
     -- Given a hypothesis, returns Nothing when equivalence or a (equivariant)
     -- set of counter examples. Needs to be quantified over q, because the
@@ -50,6 +53,8 @@ foreachQuery f qs = map (\q -> (q, f q)) qs
 -- 1. Fully automatic
 -- 2. Fully interactive (via IO)
 -- 3. Automatic membership, but interactive equivalence tests
+-- Furthermore we provide a teacher which counts and then passes the query
+-- to a delegate.
 
 -- 1. This is a fully automatic teacher, which has an internal automaton
 -- Only works for DFAs for now, as those can be checked for equivalence
@@ -61,7 +66,7 @@ teacherWithTarget aut = Teacher
     }
 
 -- 1b. This is a fully automatic teacher, which has an internal automaton
--- Might work for NFAs, not really tested
+-- NFA have undecidable equivalence, n is a bound on deoth of bisimulation.
 teacherWithTargetNonDet :: (Show i, Show q, NominalType i, NominalType q) => Int -> Automaton q i -> Teacher i
 teacherWithTargetNonDet n aut = Teacher
     { membership = foreachQuery $ automaticMembership aut
@@ -82,7 +87,8 @@ teacherWithIO = Teacher
     }
 
 -- 3. A teacher uses a target for the mebership queries, but you for equivalence
--- Useful as long as you don't have an equivalence check, For example for G-NFAs
+-- Useful as long as you don't have an equivalence check
+-- used for NFAs when there was no bounded bisimulation yet
 teacherWithTargetAndIO :: NominalType q => Automaton q Atom -> Teacher Atom
 teacherWithTargetAndIO aut = Teacher
     { membership = foreachQuery $ automaticMembership aut
@@ -131,7 +137,9 @@ mqCounter :: IORef [Int]
 {-# NOINLINE mqCounter #-}
 mqCounter = unsafePerformIO $ newIORef []
 
+
 -- Implementations of above functions
+-- 
 automaticMembership aut input = accepts aut input
 automaticEquivalent bisimlator aut hypo = case solve isEq of
         Nothing -> error "should be solved"
@@ -146,8 +154,7 @@ automaticAlphabet aut = NLambda.alphabet aut
 instance Conditional a => Conditional (Identity a) where
     cond f x y = return (cond f (runIdentity x) (runIdentity y))
 
--- Checks bisimulation of initial states
--- I am not sure whether it does the right thing for non-det automata
+-- Checks bisimulation of initial states (only for DFAs)
 -- returns some counter examples if not bisimilar
 -- returns empty set iff bisimilar
 bisim :: (NominalType i, NominalType q1, NominalType q2) => Automaton q1 i -> Automaton q2 i -> Set [i]
@@ -219,6 +226,7 @@ bisimNonDet n aut1 aut2 = runIdentity $ go empty (singleton ([], initialStates a
         addEmptyWord x y = ([], x, y)
         sumMap f = sum . (map f)
 
+-- Posing a membership query to the terminal and waits for used to input a formula
 ioMembership :: (Show i, NominalType i) => [i] -> Formula
 ioMembership input = unsafePerformIO $ do
     let supp = leastSupport input
@@ -243,6 +251,7 @@ ioMembership input = unsafePerformIO $ do
                             loop
                         Just f -> return f
 
+-- Poses a query to the terminal, waiting for the user to provide a counter example
 ioEquivalent :: (Show q, NominalType q) => Automaton q Atom -> Maybe (Set [Atom])
 ioEquivalent hypothesis = unsafePerformIO $ do
     Prelude.putStrLn "\n# Is the following automaton correct?"