diff options
Diffstat (limited to 'tools/coqc.ml')
| -rw-r--r-- | tools/coqc.ml | 29 |
1 files changed, 17 insertions, 12 deletions
diff --git a/tools/coqc.ml b/tools/coqc.ml index b12d4871..90d8e67c 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Coq compiler : coqc *) @@ -77,25 +79,28 @@ let parse_args () = | ("-v"|"--version") :: _ -> Usage.version 0 | ("-where") :: _ -> - Envars.set_coqlib (fun x -> x); + Envars.set_coqlib ~fail:(fun x -> x); print_endline (Envars.coqlib ()); exit 0 | ("-config" | "--config") :: _ -> - Envars.set_coqlib (fun x -> x); - Usage.print_config (); + Envars.set_coqlib ~fail:(fun x -> x); + Envars.print_config stdout Coq_config.all_src_dirs; exit 0 + + | ("-print-version" | "--print-version") :: _ -> + Usage.machine_readable_version 0 (* Options for coqtop : a) options with 0 argument *) - | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac" + | ("-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac" |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob" - |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" - |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit" - |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs" + |"-q"|"-profile"|"-echo" |"-quiet" + |"-silent"|"-m"|"-beautify"|"-strict-implicit" |"-impredicative-set"|"-vm"|"-native-compiler" |"-indices-matter"|"-quick"|"-type-in-type" |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch" + |"-stm-debug" as o) :: rem -> parse (cfiles,o::args) rem @@ -106,7 +111,7 @@ let parse_args () = |"-load-ml-source"|"-require"|"-load-ml-object" |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top" |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w" - |"-o"|"-profile-ltac-cutoff" + |"-o"|"-profile-ltac-cutoff"|"-mangle-names" as o) :: rem -> begin match rem with |