aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-10-08 10:33:13 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-10-08 10:33:13 +0000
commit63e4c65712e6f7b35434dc10f6ad892c4ae5cd04 (patch)
tree0c9524994e10d1bbefa35045c21e8c36711081f9 /toplevel
parent402dbb2ac9632e5745f194e891ea09a16a282084 (diff)
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
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqtop.ml4
1 files changed, 2 insertions, 2 deletions
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 ->