Merge pull request #17 from ayberkt/develop

Avoid non-exhaustive matching (and thus warnings)

src/flags.sml

@@ -12,7 +12,9 @@ structure Flags : FLAGS = struct
   fun parseArgs [] = ()
     | parseArgs ("--latex"::rest) =
         (flgShouldGenLaTeX := true; parseArgs rest)
-    | parseArgs ("--steps"::rest) = parseArgs rest
     | parseArgs ("--out"::file::rest) =
         (flgOutFile := SOME file; parseArgs rest)
+    | parseArgs (arg::_) =
+        (print ("Unrecognized argument: " ^ arg ^ "\n");
+         OS.Process.exit OS.Process.failure)
 end

src/ljt.sml

@@ -123,6 +123,7 @@ structure LJT = struct
                  OneInf (DisjR2, breakdown (G || [] ===> B), goal))
         end
     | breakdown (G || [] ===> C) = searchSync G C
+    | breakdown _ = raise Fail "breakdown case not supposed to happen"
 
   and searchSync G C =
     case getSome (eliminate C) (allCtxs G) of