(lang dune 3.23)
(name rocq-micromega-plugin)
(sections
 (lib /usr/lib/powerpc64le-linux-gnu/ocaml/5.4.1/rocq-micromega-plugin)
 (lib_root /usr/lib/powerpc64le-linux-gnu/ocaml/5.4.1)
 (libexec /usr/lib/powerpc64le-linux-gnu/ocaml/5.4.1/rocq-micromega-plugin)
 (doc /usr/doc/rocq-micromega-plugin))
(files
 (lib
  (META
   dune-package
   opam
   plugin/certificate.ml
   plugin/certificate.mli
   plugin/coq_micromega.ml
   plugin/coq_micromega.mli
   plugin/g_micromega.ml
   plugin/g_micromega.mli
   plugin/itv.ml
   plugin/itv.mli
   plugin/linsolve.ml
   plugin/linsolve.mli
   plugin/micromega.ml
   plugin/micromega.mli
   plugin/micromega_ml_plugin.a
   plugin/micromega_ml_plugin.cma
   plugin/micromega_ml_plugin.cmi
   plugin/micromega_ml_plugin.cmt
   plugin/micromega_ml_plugin.cmx
   plugin/micromega_ml_plugin.cmxa
   plugin/micromega_ml_plugin.ml
   plugin/micromega_ml_plugin__Certificate.cmi
   plugin/micromega_ml_plugin__Certificate.cmt
   plugin/micromega_ml_plugin__Certificate.cmti
   plugin/micromega_ml_plugin__Certificate.cmx
   plugin/micromega_ml_plugin__Coq_micromega.cmi
   plugin/micromega_ml_plugin__Coq_micromega.cmt
   plugin/micromega_ml_plugin__Coq_micromega.cmti
   plugin/micromega_ml_plugin__Coq_micromega.cmx
   plugin/micromega_ml_plugin__G_micromega.cmi
   plugin/micromega_ml_plugin__G_micromega.cmt
   plugin/micromega_ml_plugin__G_micromega.cmti
   plugin/micromega_ml_plugin__G_micromega.cmx
   plugin/micromega_ml_plugin__Itv.cmi
   plugin/micromega_ml_plugin__Itv.cmt
   plugin/micromega_ml_plugin__Itv.cmti
   plugin/micromega_ml_plugin__Itv.cmx
   plugin/micromega_ml_plugin__Linsolve.cmi
   plugin/micromega_ml_plugin__Linsolve.cmt
   plugin/micromega_ml_plugin__Linsolve.cmti
   plugin/micromega_ml_plugin__Linsolve.cmx
   plugin/micromega_ml_plugin__Micromega.cmi
   plugin/micromega_ml_plugin__Micromega.cmt
   plugin/micromega_ml_plugin__Micromega.cmti
   plugin/micromega_ml_plugin__Micromega.cmx
   plugin/micromega_ml_plugin__Mutils.cmi
   plugin/micromega_ml_plugin__Mutils.cmt
   plugin/micromega_ml_plugin__Mutils.cmti
   plugin/micromega_ml_plugin__Mutils.cmx
   plugin/micromega_ml_plugin__NumCompat.cmi
   plugin/micromega_ml_plugin__NumCompat.cmt
   plugin/micromega_ml_plugin__NumCompat.cmti
   plugin/micromega_ml_plugin__NumCompat.cmx
   plugin/micromega_ml_plugin__Persistent_cache.cmi
   plugin/micromega_ml_plugin__Persistent_cache.cmt
   plugin/micromega_ml_plugin__Persistent_cache.cmti
   plugin/micromega_ml_plugin__Persistent_cache.cmx
   plugin/micromega_ml_plugin__Polynomial.cmi
   plugin/micromega_ml_plugin__Polynomial.cmt
   plugin/micromega_ml_plugin__Polynomial.cmti
   plugin/micromega_ml_plugin__Polynomial.cmx
   plugin/micromega_ml_plugin__Simplex.cmi
   plugin/micromega_ml_plugin__Simplex.cmt
   plugin/micromega_ml_plugin__Simplex.cmti
   plugin/micromega_ml_plugin__Simplex.cmx
   plugin/micromega_ml_plugin__Sos.cmi
   plugin/micromega_ml_plugin__Sos.cmt
   plugin/micromega_ml_plugin__Sos.cmti
   plugin/micromega_ml_plugin__Sos.cmx
   plugin/micromega_ml_plugin__Sos_lib.cmi
   plugin/micromega_ml_plugin__Sos_lib.cmt
   plugin/micromega_ml_plugin__Sos_lib.cmti
   plugin/micromega_ml_plugin__Sos_lib.cmx
   plugin/micromega_ml_plugin__Sos_types.cmi
   plugin/micromega_ml_plugin__Sos_types.cmt
   plugin/micromega_ml_plugin__Sos_types.cmti
   plugin/micromega_ml_plugin__Sos_types.cmx
   plugin/micromega_ml_plugin__Vect.cmi
   plugin/micromega_ml_plugin__Vect.cmt
   plugin/micromega_ml_plugin__Vect.cmti
   plugin/micromega_ml_plugin__Vect.cmx
   plugin/mutils.ml
   plugin/mutils.mli
   plugin/numCompat.ml
   plugin/numCompat.mli
   plugin/persistent_cache.ml
   plugin/persistent_cache.mli
   plugin/polynomial.ml
   plugin/polynomial.mli
   plugin/simplex.ml
   plugin/simplex.mli
   plugin/sos.ml
   plugin/sos.mli
   plugin/sos_lib.ml
   plugin/sos_lib.mli
   plugin/sos_types.ml
   plugin/sos_types.mli
   plugin/vect.ml
   plugin/vect.mli
   zify/g_zify.ml
   zify/g_zify.mli
   zify/zify.ml
   zify/zify.mli
   zify/zify_ml_plugin.a
   zify/zify_ml_plugin.cma
   zify/zify_ml_plugin.cmi
   zify/zify_ml_plugin.cmt
   zify/zify_ml_plugin.cmx
   zify/zify_ml_plugin.cmxa
   zify/zify_ml_plugin.ml
   zify/zify_ml_plugin__G_zify.cmi
   zify/zify_ml_plugin__G_zify.cmt
   zify/zify_ml_plugin__G_zify.cmti
   zify/zify_ml_plugin__G_zify.cmx
   zify/zify_ml_plugin__Zify.cmi
   zify/zify_ml_plugin__Zify.cmt
   zify/zify_ml_plugin__Zify.cmti
   zify/zify_ml_plugin__Zify.cmx))
 (lib_root
  (coq/user-contrib/micromega_plugin/ListDef.glob
   coq/user-contrib/micromega_plugin/ListDef.v
   coq/user-contrib/micromega_plugin/ListDef.vo
   coq/user-contrib/micromega_plugin/NatDef.glob
   coq/user-contrib/micromega_plugin/NatDef.v
   coq/user-contrib/micromega_plugin/NatDef.vo
   coq/user-contrib/micromega_plugin/PosDef.glob
   coq/user-contrib/micromega_plugin/PosDef.v
   coq/user-contrib/micromega_plugin/PosDef.vo
   coq/user-contrib/micromega_plugin/RatDef.glob
   coq/user-contrib/micromega_plugin/RatDef.v
   coq/user-contrib/micromega_plugin/RatDef.vo
   coq/user-contrib/micromega_plugin/Zify.glob
   coq/user-contrib/micromega_plugin/Zify.v
   coq/user-contrib/micromega_plugin/Zify.vo
   coq/user-contrib/micromega_plugin/checker.glob
   coq/user-contrib/micromega_plugin/checker.v
   coq/user-contrib/micromega_plugin/checker.vo
   coq/user-contrib/micromega_plugin/eval.glob
   coq/user-contrib/micromega_plugin/eval.v
   coq/user-contrib/micromega_plugin/eval.vo
   coq/user-contrib/micromega_plugin/field_checker.glob
   coq/user-contrib/micromega_plugin/field_checker.v
   coq/user-contrib/micromega_plugin/field_checker.vo
   coq/user-contrib/micromega_plugin/field_eval.glob
   coq/user-contrib/micromega_plugin/field_eval.v
   coq/user-contrib/micromega_plugin/field_eval.vo
   coq/user-contrib/micromega_plugin/formula.glob
   coq/user-contrib/micromega_plugin/formula.v
   coq/user-contrib/micromega_plugin/formula.vo
   coq/user-contrib/micromega_plugin/micromega_ml_plugin.cmxs
   coq/user-contrib/micromega_plugin/ring_checker.glob
   coq/user-contrib/micromega_plugin/ring_checker.v
   coq/user-contrib/micromega_plugin/ring_checker.vo
   coq/user-contrib/micromega_plugin/ring_eval.glob
   coq/user-contrib/micromega_plugin/ring_eval.v
   coq/user-contrib/micromega_plugin/ring_eval.vo
   coq/user-contrib/micromega_plugin/tactics.glob
   coq/user-contrib/micromega_plugin/tactics.v
   coq/user-contrib/micromega_plugin/tactics.vo
   coq/user-contrib/micromega_plugin/witness.glob
   coq/user-contrib/micromega_plugin/witness.v
   coq/user-contrib/micromega_plugin/witness.vo
   coq/user-contrib/micromega_plugin/zify_ml_plugin.cmxs))
 (libexec (plugin/micromega_ml_plugin.cmxs zify/zify_ml_plugin.cmxs))
 (doc (LICENSE README-developers.md README.md)))
(library
 (name rocq-micromega-plugin.plugin)
 (kind normal)
 (archives
  (byte plugin/micromega_ml_plugin.cma)
  (native plugin/micromega_ml_plugin.cmxa))
 (plugins
  (byte plugin/micromega_ml_plugin.cma)
  (native plugin/micromega_ml_plugin.cmxs))
 (native_archives plugin/micromega_ml_plugin.a)
 (requires rocq-runtime.plugins.ltac rocq-runtime.vernac)
 (main_module_name Micromega_ml_plugin)
 (modes byte native)
 (modules
  (wrapped
   (group
    (alias
     (obj_name micromega_ml_plugin)
     (visibility public)
     (kind alias)
     (source
      (path Micromega_ml_plugin)
      (impl (path plugin/micromega_ml_plugin.ml-gen))))
    (name Micromega_ml_plugin)
    (modules
     (module
      (obj_name micromega_ml_plugin__Certificate)
      (visibility public)
      (source
       (path Certificate)
       (intf (path plugin/certificate.mli))
       (impl (path plugin/certificate.ml))))
     (module
      (obj_name micromega_ml_plugin__Coq_micromega)
      (visibility public)
      (source
       (path Coq_micromega)
       (intf (path plugin/coq_micromega.mli))
       (impl (path plugin/coq_micromega.ml))))
     (module
      (obj_name micromega_ml_plugin__G_micromega)
      (visibility public)
      (source
       (path G_micromega)
       (intf (path plugin/g_micromega.mli))
       (impl (path plugin/g_micromega.ml))))
     (module
      (obj_name micromega_ml_plugin__Itv)
      (visibility public)
      (source
       (path Itv)
       (intf (path plugin/itv.mli))
       (impl (path plugin/itv.ml))))
     (module
      (obj_name micromega_ml_plugin__Linsolve)
      (visibility public)
      (source
       (path Linsolve)
       (intf (path plugin/linsolve.mli))
       (impl (path plugin/linsolve.ml))))
     (module
      (obj_name micromega_ml_plugin__Micromega)
      (visibility public)
      (source
       (path Micromega)
       (intf (path plugin/micromega.mli))
       (impl (path plugin/micromega.ml))))
     (module
      (obj_name micromega_ml_plugin__Mutils)
      (visibility public)
      (source
       (path Mutils)
       (intf (path plugin/mutils.mli))
       (impl (path plugin/mutils.ml))))
     (module
      (obj_name micromega_ml_plugin__NumCompat)
      (visibility public)
      (source
       (path NumCompat)
       (intf (path plugin/numCompat.mli))
       (impl (path plugin/numCompat.ml))))
     (module
      (obj_name micromega_ml_plugin__Persistent_cache)
      (visibility public)
      (source
       (path Persistent_cache)
       (intf (path plugin/persistent_cache.mli))
       (impl (path plugin/persistent_cache.ml))))
     (module
      (obj_name micromega_ml_plugin__Polynomial)
      (visibility public)
      (source
       (path Polynomial)
       (intf (path plugin/polynomial.mli))
       (impl (path plugin/polynomial.ml))))
     (module
      (obj_name micromega_ml_plugin__Simplex)
      (visibility public)
      (source
       (path Simplex)
       (intf (path plugin/simplex.mli))
       (impl (path plugin/simplex.ml))))
     (module
      (obj_name micromega_ml_plugin__Sos)
      (visibility public)
      (source
       (path Sos)
       (intf (path plugin/sos.mli))
       (impl (path plugin/sos.ml))))
     (module
      (obj_name micromega_ml_plugin__Sos_lib)
      (visibility public)
      (source
       (path Sos_lib)
       (intf (path plugin/sos_lib.mli))
       (impl (path plugin/sos_lib.ml))))
     (module
      (obj_name micromega_ml_plugin__Sos_types)
      (visibility public)
      (source
       (path Sos_types)
       (intf (path plugin/sos_types.mli))
       (impl (path plugin/sos_types.ml))))
     (module
      (obj_name micromega_ml_plugin__Vect)
      (visibility public)
      (source
       (path Vect)
       (intf (path plugin/vect.mli))
       (impl (path plugin/vect.ml))))))
   (wrapped true))))
(library
 (name rocq-micromega-plugin.zify)
 (kind normal)
 (archives (byte zify/zify_ml_plugin.cma) (native zify/zify_ml_plugin.cmxa))
 (plugins (byte zify/zify_ml_plugin.cma) (native zify/zify_ml_plugin.cmxs))
 (native_archives zify/zify_ml_plugin.a)
 (requires rocq-runtime.plugins.ltac)
 (main_module_name Zify_ml_plugin)
 (modes byte native)
 (modules
  (wrapped
   (group
    (alias
     (obj_name zify_ml_plugin)
     (visibility public)
     (kind alias)
     (source (path Zify_ml_plugin) (impl (path zify/zify_ml_plugin.ml-gen))))
    (name Zify_ml_plugin)
    (modules
     (module
      (obj_name zify_ml_plugin__G_zify)
      (visibility public)
      (source
       (path G_zify)
       (intf (path zify/g_zify.mli))
       (impl (path zify/g_zify.ml))))
     (module
      (obj_name zify_ml_plugin__Zify)
      (visibility public)
      (source
       (path Zify)
       (intf (path zify/zify.mli))
       (impl (path zify/zify.ml))))))
   (wrapped true))))
