| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/plugins/extraction/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 1 kB |
|
Quelle extract_env.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) *) (************************************************************************) (*s This module declares the extraction commands. *) open Names open Libnames val simple_extraction : opaque_access:Global.indirect_accessor -> qualid -> unit val full_extraction : opaque_access:Global.indirect_accessor -> string option -> qualid lis val separate_extraction : opaque_access:Global.indirect_accessor -> qualid list -> unit val extraction_library : opaque_access:Global.indirect_accessor -> bool -> lident -> unit (* For the test-suite : extraction to a temporary file + ocamlc on it *) val extract_and_compile : opaque_access:Global.indirect_accessor -> qualid list -> unit (* For debug / external output via coqtop.byte + Drop : *) val mono_environment : Common.State.t -> opaque_access:Global.indirect_accessor -> Miniml.global list -> ModPath. (* Used by the Relation Extraction plugin *) val print_one_decl : Common.State.t -> Miniml.ml_structure -> ModPath.t -> Miniml.ml_decl -> Pp.t (* Show the extraction of the current ongoing proof *) val show_extraction : pstate:Declare.Proof.t -> unit ¤ Dauer der Verarbeitung: 0.3 Sekunden ¤*© Formatika GbR, Deutschland |
|
2026-03-28