Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
UsePluginWarning.v
Sprache: Unknown
|
(* -*- mode: coq; coq-prog-args: ("-w" "-extraction-logical-axiom") -*- *)
Require Extraction.
Axiom foo : Prop.
Extraction foo.
[ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
]
|
