From 63e4c65712e6f7b35434dc10f6ad892c4ae5cd04 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 8 Oct 2003 10:33:13 +0000 Subject: Renommage no-strict en -strict-implicit; option -dont-load-proofs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4540 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/coqtop.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'toplevel/coqtop.ml') diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 1d8b4de63..6cb8ddb29 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -182,7 +182,7 @@ let parse_args is_ide = | "-compile-verbose" :: f :: rem -> add_compile true f; parse rem | "-compile-verbose" :: [] -> usage () - | "-no-proofs" :: rem -> Options.dont_load_proofs := true; parse rem + | "-dont-load-proofs" :: rem -> Options.dont_load_proofs := true; parse rem | "-translate" :: rem -> make_translate true; parse rem @@ -220,7 +220,7 @@ let parse_args is_ide = | "-v8" :: rem -> (* Options.v7 := false; *) parse rem (* Translator options *) - | "-no-strict" :: rem -> + | "-strict-implicit" :: rem -> Options.translate_strict_impargs := false; parse rem | s :: rem -> -- cgit v1.2.3