; For now we use coq_dune to generate the rules here
(coq.theory
 (name Corelib)
 (package rocq-core)
 (synopsis "Rocq's Core Library")
 ; Uncomment this to have dune compile native files in release mode
 ; (mode native)
 (boot)
 (plugins
   rocq-runtime.plugins.ltac
   rocq-runtime.plugins.tauto

   rocq-runtime.plugins.cc
   rocq-runtime.plugins.firstorder

   rocq-runtime.plugins.number_string_notation

   rocq-runtime.plugins.btauto
   rocq-runtime.plugins.rtauto

   rocq-runtime.plugins.ring
   rocq-runtime.plugins.nsatz

   rocq-runtime.plugins.zify
   rocq-runtime.plugins.micromega

   rocq-runtime.plugins.funind

   rocq-runtime.plugins.ssreflect
   rocq-runtime.plugins.derive))

(include_subdirs qualified)

(documentation
 (package rocq-core))