| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/boot/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 1 kB |
|
Quelle util.mli Sprache: SML |
|||||||||
|
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * 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) *) (************************************************************************) val getenv_opt : string -> string option val getenv_rocq : string -> string option (** [getenv_rocq name] returns the value of "ROCQ$name" if it exists, otherwise the value of "COQ$name" if it exists and warns that it is deprecated, otherwise [None]. *) val getenv_rocq_gen : rocq:string -> coq:string -> string option (** [getenv_rocq_gen ~rocq ~coq] returns the value of [rocq] if it exists, otherwise the value of [coq] if it exists and warns that it is deprecated, otherwise [None]. *) val set_warn_deprecated_coq_var : (rocq:string -> coq:string -> unit) -> unit ¤ Dauer der Verarbeitung: 0.25 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28