diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-08 10:33:13 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-08 10:33:13 +0000 |
| commit | 63e4c65712e6f7b35434dc10f6ad892c4ae5cd04 (patch) | |
| tree | 0c9524994e10d1bbefa35045c21e8c36711081f9 | |
| parent | 402dbb2ac9632e5745f194e891ea09a16a282084 (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
| -rw-r--r-- | scripts/coqc.ml | 5 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 4 |
2 files changed, 5 insertions, 4 deletions
diff --git a/scripts/coqc.ml b/scripts/coqc.ml index 692b86c16..d35141f97 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -127,7 +127,7 @@ let parse_args () = | ("-libdir"|"-I"|"-include"|"-outputstate" |"-inputstate"|"-is"|"-load-vernac-source"|"-load-vernac-object" |"-load-ml-source"|"-require"|"-load-ml-object"|"-user" - |"-init-file"|"-dump-glob"|"-no-strict" as o) :: rem -> + |"-init-file"|"-dump-glob" as o) :: rem -> begin match rem with | s :: rem' -> parse (cfiles,s::o::args) rem' @@ -136,7 +136,8 @@ let parse_args () = | "-R" as o :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem | ("-notactics"|"-debug"|"-db"|"-debugger"|"-nolib"|"-batch"|"-nois" |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" - |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-translate" as o) :: rem -> + |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-translate"|"strict-implicit" + |"-dont-load-proofs" as o) :: rem -> parse (cfiles,o::args) rem | ("-v"|"--version") :: _ -> Usage.version () 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 -> |