Eine aufbereitete Darstellung der Quelle

 
     
 
 
Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 

Benutzer

Quelle  META.rocq-plugin-tutorial   Sprache: unbekannt

 
Spracherkennung für: .rocq-plugin-tutorial vermutete Sprache: Unknown {[0] [0] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]

# Comments in META start with # and end with newline

# our plugin is called rocq-plugin-tutorial.tuto1
# rocq-plugin-tutorial from the META filename
# tuto1 from this "package" name
package "tuto1" (
    # the plugin files are in "src"
    directory = "src"

    version = "dev"
    description = "A tuto1 plugin"

    # we define ltac1 tactics so we depend on ltac
    # otherwise we would depend only on rocq-runtime.vernac
    # (it contains the APIs for declaring new commands)
    # (ltac depends on vernac so if we depend on ltac, vernac is also implicitly depended on)
    requires = "rocq-runtime.plugins.ltac"

    # the compiled plugin files (rocq makefile bases these filenames on the .mlpack filename)
    # (only the "plugin" keys are used by rocq,
    # "archive" is for packages which depend on this package)
    archive(byte) = "tuto1_plugin.cma"
    archive(native) = "tuto1_plugin.cmxa"
    plugin(byte) = "tuto1_plugin.cma"
    plugin(native) = "tuto1_plugin.cmxs"
)

# paths in this file are relative to this directory
directory = "."

[Dauer der Verarbeitung: 0.12 Sekunden, vorverarbeitet 2026-06-17]

                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Open Source Software

     Quellcodebibliothek
     Eigene Quellcodes
     Fremde Quellcodes
     Suchen

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik

Statistik
#Sources=141584
#Domains=738142