diff --git a/src/flags.sml b/src/flags.sml index df21c8f..2f12c21 100644 --- a/src/flags.sml +++ b/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 diff --git a/src/ljt.sml b/src/ljt.sml index d4a0c16..8237a7e 100644 --- a/src/ljt.sml +++ b/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