From d8324290e855b2d36e906599c7598fe5ebedb299 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 23 Apr 2013 18:15:43 +0000 Subject: Remove deprecated option -no-hash-consing (currently doing nothing) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16442 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/checker.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'checker') diff --git a/checker/checker.ml b/checker/checker.ml index e981cf8fea..280f346568 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 () -- cgit v1.2.3