description = "The Rocq Prover's Core library (including Prelude)."
rocqpath = "Corelib"
requires = "rocq-runtime.plugins.ltac"
requires += "rocq-runtime.plugins.tauto"
requires += "rocq-runtime.plugins.cc"
requires += "rocq-runtime.plugins.firstorder"
requires += "rocq-runtime.plugins.number_string_notation"
requires += "rocq-runtime.plugins.btauto"
requires += "rocq-runtime.plugins.rtauto"
requires += "rocq-runtime.plugins.ring"
requires += "rocq-runtime.plugins.nsatz"
requires += "rocq-runtime.plugins.zify"
requires += "rocq-runtime.plugins.micromega"
requires += "rocq-runtime.plugins.funind"
requires += "rocq-runtime.plugins.ssreflect"
requires += "rocq-runtime.plugins.derive"
package "ltac2" (
  directory = "ltac2"
  description = "The Rocq Prover's Ltac2 standard library."
  rocqpath = "Ltac2"
  requires = "rocq-core"
  requires += "rocq-runtime.plugins.ltac2_ltac1"
  requires += "rocq-runtime.plugins.ltac2"
)