aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/checker.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/checker.ml')
-rw-r--r--checker/checker.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/checker/checker.ml b/checker/checker.ml
index e981cf8fe..280f34656 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -316,8 +316,6 @@ let parse_args argv =
| ("-o" | "--output-context") :: rem ->
Check_stat.output_context := true; parse rem
- | "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem
-
| "-admit" :: s :: rem -> add_admit s; parse rem
| "-admit" :: [] -> usage ()