2 files changed, 1 insertions, 48 deletions
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs
index 84baa12..d769afe 100644
--- a/source/Syntax/Internal.hs
+++ b/source/Syntax/Internal.hs
@@ -777,53 +777,6 @@ data Block
     deriving (Show, Eq, Ord)
 
 
-data Task = Task
-    { taskDirectness :: Directness
-    , taskHypotheses :: [Hypothesis] -- ^ No guarantees on order.
-    , taskConjectureLabel :: Marker
-    , taskLocation :: Location
-    , taskConjecture :: Formula
-    } deriving (Show, Eq, Generic, Hashable)
-
-data Hypothesis = Hypothesis
-    { hypothesisMarker :: Marker
-    , hypothesisFormula :: Formula
-    }
-
-instance Show Hypothesis where
-    show (Hypothesis marker formula) =
-        "Hypothesis " <> show marker <> " " <> show formula
-
-instance Eq Hypothesis where
-    Hypothesis marker formula == Hypothesis marker' formula' =
-        (marker, formula) == (marker', formula')
-
-instance Ord Hypothesis where
-    compare (Hypothesis marker formula) (Hypothesis marker' formula') =
-        compare (marker, formula) (marker', formula')
-
-instance Hashable Hypothesis where
-    hashWithSalt salt (Hypothesis marker formula) =
-        hashWithSalt salt (marker, formula)
-
-
--- | Indicates whether a given proof is direct or indirect.
--- An indirect proof (i.e. a proof by contradiction) may
--- cause an ATP to emit a warning about contradictory axioms.
--- When we know that the proof is indirect, we want to ignore
--- this warning. For relevance filtering we also want to know
--- what our actual goal is, so we keep the original conjecture.
-data Directness
-    = Indirect Formula -- ^ The former conjecture.
-    | Direct
-    deriving (Show, Eq, Generic, Hashable)
-
-isIndirect :: Task -> Bool
-isIndirect task = case taskDirectness task of
-    Indirect _ -> True
-    Direct -> False
-
-
 -- | Full boolean contraction.
 contraction :: ExprOf a -> ExprOf a
 contraction = \case
diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs
index 408b374..5dfed65 100644
--- a/source/Syntax/Token.hs
+++ b/source/Syntax/Token.hs
@@ -354,7 +354,7 @@ beginToplevelEnvironment = lexeme do
 -- | Parses tokens, switching tokenizing frames when encountering math and text environments.
 environment :: Lexer [Located Token]
 environment = do
-    env <- skipManyTill anySingle beginToplevelEnvironment
+    env <- skipManyTill (comment <|> void anySingle) beginToplevelEnvironment
     lts <- go (unLocated env) id
     pure ((BeginEnv <$> env) : lts)
     where