(lang dune 3.23)
(name rocq-equations)
(sections
 (lib /usr/lib/x86_64-linux-gnu/ocaml/5.4.1/rocq-equations)
 (lib_root /usr/lib/x86_64-linux-gnu/ocaml/5.4.1)
 (libexec /usr/lib/x86_64-linux-gnu/ocaml/5.4.1/rocq-equations)
 (doc /usr/doc/rocq-equations))
(files
 (lib
  (META
   dune-package
   opam
   plugin/context_map.ml
   plugin/context_map.mli
   plugin/covering.ml
   plugin/covering.mli
   plugin/depelim.ml
   plugin/depelim.mli
   plugin/ederive.ml
   plugin/ederive.mli
   plugin/eqdec.ml
   plugin/eqdec.mli
   plugin/equations.ml
   plugin/equations.mli
   plugin/equations_common.ml
   plugin/equations_common.mli
   plugin/equations_plugin.a
   plugin/equations_plugin.cma
   plugin/equations_plugin.cmi
   plugin/equations_plugin.cmt
   plugin/equations_plugin.cmx
   plugin/equations_plugin.cmxa
   plugin/equations_plugin.ml
   plugin/equations_plugin__Context_map.cmi
   plugin/equations_plugin__Context_map.cmt
   plugin/equations_plugin__Context_map.cmti
   plugin/equations_plugin__Context_map.cmx
   plugin/equations_plugin__Covering.cmi
   plugin/equations_plugin__Covering.cmt
   plugin/equations_plugin__Covering.cmti
   plugin/equations_plugin__Covering.cmx
   plugin/equations_plugin__Depelim.cmi
   plugin/equations_plugin__Depelim.cmt
   plugin/equations_plugin__Depelim.cmti
   plugin/equations_plugin__Depelim.cmx
   plugin/equations_plugin__Ederive.cmi
   plugin/equations_plugin__Ederive.cmt
   plugin/equations_plugin__Ederive.cmti
   plugin/equations_plugin__Ederive.cmx
   plugin/equations_plugin__Eqdec.cmi
   plugin/equations_plugin__Eqdec.cmt
   plugin/equations_plugin__Eqdec.cmti
   plugin/equations_plugin__Eqdec.cmx
   plugin/equations_plugin__Equations.cmi
   plugin/equations_plugin__Equations.cmt
   plugin/equations_plugin__Equations.cmti
   plugin/equations_plugin__Equations.cmx
   plugin/equations_plugin__Equations_common.cmi
   plugin/equations_plugin__Equations_common.cmt
   plugin/equations_plugin__Equations_common.cmti
   plugin/equations_plugin__Equations_common.cmx
   plugin/equations_plugin__Extra_tactics.cmi
   plugin/equations_plugin__Extra_tactics.cmt
   plugin/equations_plugin__Extra_tactics.cmti
   plugin/equations_plugin__Extra_tactics.cmx
   plugin/equations_plugin__G_equations.cmi
   plugin/equations_plugin__G_equations.cmt
   plugin/equations_plugin__G_equations.cmx
   plugin/equations_plugin__Noconf.cmi
   plugin/equations_plugin__Noconf.cmt
   plugin/equations_plugin__Noconf.cmti
   plugin/equations_plugin__Noconf.cmx
   plugin/equations_plugin__Noconf_hom.cmi
   plugin/equations_plugin__Noconf_hom.cmt
   plugin/equations_plugin__Noconf_hom.cmti
   plugin/equations_plugin__Noconf_hom.cmx
   plugin/equations_plugin__Principles.cmi
   plugin/equations_plugin__Principles.cmt
   plugin/equations_plugin__Principles.cmti
   plugin/equations_plugin__Principles.cmx
   plugin/equations_plugin__Principles_proofs.cmi
   plugin/equations_plugin__Principles_proofs.cmt
   plugin/equations_plugin__Principles_proofs.cmti
   plugin/equations_plugin__Principles_proofs.cmx
   plugin/equations_plugin__Sigma_types.cmi
   plugin/equations_plugin__Sigma_types.cmt
   plugin/equations_plugin__Sigma_types.cmti
   plugin/equations_plugin__Sigma_types.cmx
   plugin/equations_plugin__Simplify.cmi
   plugin/equations_plugin__Simplify.cmt
   plugin/equations_plugin__Simplify.cmti
   plugin/equations_plugin__Simplify.cmx
   plugin/equations_plugin__Splitting.cmi
   plugin/equations_plugin__Splitting.cmt
   plugin/equations_plugin__Splitting.cmti
   plugin/equations_plugin__Splitting.cmx
   plugin/equations_plugin__Subterm.cmi
   plugin/equations_plugin__Subterm.cmt
   plugin/equations_plugin__Subterm.cmti
   plugin/equations_plugin__Subterm.cmx
   plugin/equations_plugin__Syntax.cmi
   plugin/equations_plugin__Syntax.cmt
   plugin/equations_plugin__Syntax.cmti
   plugin/equations_plugin__Syntax.cmx
   plugin/extra_tactics.ml
   plugin/extra_tactics.mli
   plugin/g_equations.ml
   plugin/noconf.ml
   plugin/noconf.mli
   plugin/noconf_hom.ml
   plugin/noconf_hom.mli
   plugin/principles.ml
   plugin/principles.mli
   plugin/principles_proofs.ml
   plugin/principles_proofs.mli
   plugin/sigma_types.ml
   plugin/sigma_types.mli
   plugin/simplify.ml
   plugin/simplify.mli
   plugin/splitting.ml
   plugin/splitting.mli
   plugin/subterm.ml
   plugin/subterm.mli
   plugin/syntax.ml
   plugin/syntax.mli))
 (lib_root
  (coq/user-contrib/Equations/CoreTactics.glob
   coq/user-contrib/Equations/CoreTactics.v
   coq/user-contrib/Equations/CoreTactics.vo
   coq/user-contrib/Equations/Init.glob
   coq/user-contrib/Equations/Init.v
   coq/user-contrib/Equations/Init.vo
   coq/user-contrib/Equations/Prop/Classes.glob
   coq/user-contrib/Equations/Prop/Classes.v
   coq/user-contrib/Equations/Prop/Classes.vo
   coq/user-contrib/Equations/Prop/Constants.glob
   coq/user-contrib/Equations/Prop/Constants.v
   coq/user-contrib/Equations/Prop/Constants.vo
   coq/user-contrib/Equations/Prop/DepElim.glob
   coq/user-contrib/Equations/Prop/DepElim.v
   coq/user-contrib/Equations/Prop/DepElim.vo
   coq/user-contrib/Equations/Prop/EqDec.glob
   coq/user-contrib/Equations/Prop/EqDec.v
   coq/user-contrib/Equations/Prop/EqDec.vo
   coq/user-contrib/Equations/Prop/EqDecInstances.glob
   coq/user-contrib/Equations/Prop/EqDecInstances.v
   coq/user-contrib/Equations/Prop/EqDecInstances.vo
   coq/user-contrib/Equations/Prop/Equations.glob
   coq/user-contrib/Equations/Prop/Equations.v
   coq/user-contrib/Equations/Prop/Equations.vo
   coq/user-contrib/Equations/Prop/FunctionalInduction.glob
   coq/user-contrib/Equations/Prop/FunctionalInduction.v
   coq/user-contrib/Equations/Prop/FunctionalInduction.vo
   coq/user-contrib/Equations/Prop/Loader.glob
   coq/user-contrib/Equations/Prop/Loader.v
   coq/user-contrib/Equations/Prop/Loader.vo
   coq/user-contrib/Equations/Prop/Logic.glob
   coq/user-contrib/Equations/Prop/Logic.v
   coq/user-contrib/Equations/Prop/Logic.vo
   coq/user-contrib/Equations/Prop/NoConfusion.glob
   coq/user-contrib/Equations/Prop/NoConfusion.v
   coq/user-contrib/Equations/Prop/NoConfusion.vo
   coq/user-contrib/Equations/Prop/NoConfusion_UIP.glob
   coq/user-contrib/Equations/Prop/NoConfusion_UIP.v
   coq/user-contrib/Equations/Prop/NoConfusion_UIP.vo
   coq/user-contrib/Equations/Prop/NoCycle.glob
   coq/user-contrib/Equations/Prop/NoCycle.v
   coq/user-contrib/Equations/Prop/NoCycle.vo
   coq/user-contrib/Equations/Prop/OpaqueEquations.glob
   coq/user-contrib/Equations/Prop/OpaqueEquations.v
   coq/user-contrib/Equations/Prop/OpaqueEquations.vo
   coq/user-contrib/Equations/Prop/SigmaNotations.glob
   coq/user-contrib/Equations/Prop/SigmaNotations.v
   coq/user-contrib/Equations/Prop/SigmaNotations.vo
   coq/user-contrib/Equations/Prop/Subterm.glob
   coq/user-contrib/Equations/Prop/Subterm.v
   coq/user-contrib/Equations/Prop/Subterm.vo
   coq/user-contrib/Equations/Prop/Tactics.glob
   coq/user-contrib/Equations/Prop/Tactics.v
   coq/user-contrib/Equations/Prop/Tactics.vo
   coq/user-contrib/Equations/Prop/Telescopes.glob
   coq/user-contrib/Equations/Prop/Telescopes.v
   coq/user-contrib/Equations/Prop/Telescopes.vo
   coq/user-contrib/Equations/Prop/TransparentEquations.glob
   coq/user-contrib/Equations/Prop/TransparentEquations.v
   coq/user-contrib/Equations/Prop/TransparentEquations.vo
   coq/user-contrib/Equations/Signature.glob
   coq/user-contrib/Equations/Signature.v
   coq/user-contrib/Equations/Signature.vo
   coq/user-contrib/Equations/Type/All.glob
   coq/user-contrib/Equations/Type/All.v
   coq/user-contrib/Equations/Type/All.vo
   coq/user-contrib/Equations/Type/Classes.glob
   coq/user-contrib/Equations/Type/Classes.v
   coq/user-contrib/Equations/Type/Classes.vo
   coq/user-contrib/Equations/Type/Constants.glob
   coq/user-contrib/Equations/Type/Constants.v
   coq/user-contrib/Equations/Type/Constants.vo
   coq/user-contrib/Equations/Type/DepElim.glob
   coq/user-contrib/Equations/Type/DepElim.v
   coq/user-contrib/Equations/Type/DepElim.vo
   coq/user-contrib/Equations/Type/EqDec.glob
   coq/user-contrib/Equations/Type/EqDec.v
   coq/user-contrib/Equations/Type/EqDec.vo
   coq/user-contrib/Equations/Type/EqDecInstances.glob
   coq/user-contrib/Equations/Type/EqDecInstances.v
   coq/user-contrib/Equations/Type/EqDecInstances.vo
   coq/user-contrib/Equations/Type/FunctionalExtensionality.glob
   coq/user-contrib/Equations/Type/FunctionalExtensionality.v
   coq/user-contrib/Equations/Type/FunctionalExtensionality.vo
   coq/user-contrib/Equations/Type/FunctionalInduction.glob
   coq/user-contrib/Equations/Type/FunctionalInduction.v
   coq/user-contrib/Equations/Type/FunctionalInduction.vo
   coq/user-contrib/Equations/Type/Loader.glob
   coq/user-contrib/Equations/Type/Loader.v
   coq/user-contrib/Equations/Type/Loader.vo
   coq/user-contrib/Equations/Type/Logic.glob
   coq/user-contrib/Equations/Type/Logic.v
   coq/user-contrib/Equations/Type/Logic.vo
   coq/user-contrib/Equations/Type/NoConfusion.glob
   coq/user-contrib/Equations/Type/NoConfusion.v
   coq/user-contrib/Equations/Type/NoConfusion.vo
   coq/user-contrib/Equations/Type/Relation.glob
   coq/user-contrib/Equations/Type/Relation.v
   coq/user-contrib/Equations/Type/Relation.vo
   coq/user-contrib/Equations/Type/Relation_Properties.glob
   coq/user-contrib/Equations/Type/Relation_Properties.v
   coq/user-contrib/Equations/Type/Relation_Properties.vo
   coq/user-contrib/Equations/Type/Subterm.glob
   coq/user-contrib/Equations/Type/Subterm.v
   coq/user-contrib/Equations/Type/Subterm.vo
   coq/user-contrib/Equations/Type/Tactics.glob
   coq/user-contrib/Equations/Type/Tactics.v
   coq/user-contrib/Equations/Type/Tactics.vo
   coq/user-contrib/Equations/Type/Telescopes.glob
   coq/user-contrib/Equations/Type/Telescopes.v
   coq/user-contrib/Equations/Type/Telescopes.vo
   coq/user-contrib/Equations/Type/WellFounded.glob
   coq/user-contrib/Equations/Type/WellFounded.v
   coq/user-contrib/Equations/Type/WellFounded.vo
   coq/user-contrib/Equations/Type/WellFoundedInstances.glob
   coq/user-contrib/Equations/Type/WellFoundedInstances.v
   coq/user-contrib/Equations/Type/WellFoundedInstances.vo
   coq/user-contrib/Equations/equations_plugin.cmxs))
 (libexec (plugin/equations_plugin.cmxs))
 (doc (CHANGES.md LICENSE README.dev README.md)))
(library
 (name rocq-equations.plugin)
 (kind normal)
 (archives
  (byte plugin/equations_plugin.cma)
  (native plugin/equations_plugin.cmxa))
 (plugins
  (byte plugin/equations_plugin.cma)
  (native plugin/equations_plugin.cmxs))
 (native_archives plugin/equations_plugin.a)
 (requires rocq-runtime.plugins.cc rocq-runtime.plugins.extraction)
 (main_module_name Equations_plugin)
 (modes byte native)
 (modules
  (wrapped
   (group
    (alias
     (obj_name equations_plugin)
     (visibility public)
     (kind alias)
     (source
      (path Equations_plugin)
      (impl (path plugin/equations_plugin.ml-gen))))
    (name Equations_plugin)
    (modules
     (module
      (obj_name equations_plugin__Context_map)
      (visibility public)
      (source
       (path Context_map)
       (intf (path plugin/context_map.mli))
       (impl (path plugin/context_map.ml))))
     (module
      (obj_name equations_plugin__Covering)
      (visibility public)
      (source
       (path Covering)
       (intf (path plugin/covering.mli))
       (impl (path plugin/covering.ml))))
     (module
      (obj_name equations_plugin__Depelim)
      (visibility public)
      (source
       (path Depelim)
       (intf (path plugin/depelim.mli))
       (impl (path plugin/depelim.ml))))
     (module
      (obj_name equations_plugin__Ederive)
      (visibility public)
      (source
       (path Ederive)
       (intf (path plugin/ederive.mli))
       (impl (path plugin/ederive.ml))))
     (module
      (obj_name equations_plugin__Eqdec)
      (visibility public)
      (source
       (path Eqdec)
       (intf (path plugin/eqdec.mli))
       (impl (path plugin/eqdec.ml))))
     (module
      (obj_name equations_plugin__Equations)
      (visibility public)
      (source
       (path Equations)
       (intf (path plugin/equations.mli))
       (impl (path plugin/equations.ml))))
     (module
      (obj_name equations_plugin__Equations_common)
      (visibility public)
      (source
       (path Equations_common)
       (intf (path plugin/equations_common.mli))
       (impl (path plugin/equations_common.ml))))
     (module
      (obj_name equations_plugin__Extra_tactics)
      (visibility public)
      (source
       (path Extra_tactics)
       (intf (path plugin/extra_tactics.mli))
       (impl (path plugin/extra_tactics.ml))))
     (module
      (obj_name equations_plugin__G_equations)
      (visibility public)
      (source (path G_equations) (impl (path plugin/g_equations.ml))))
     (module
      (obj_name equations_plugin__Noconf)
      (visibility public)
      (source
       (path Noconf)
       (intf (path plugin/noconf.mli))
       (impl (path plugin/noconf.ml))))
     (module
      (obj_name equations_plugin__Noconf_hom)
      (visibility public)
      (source
       (path Noconf_hom)
       (intf (path plugin/noconf_hom.mli))
       (impl (path plugin/noconf_hom.ml))))
     (module
      (obj_name equations_plugin__Principles)
      (visibility public)
      (source
       (path Principles)
       (intf (path plugin/principles.mli))
       (impl (path plugin/principles.ml))))
     (module
      (obj_name equations_plugin__Principles_proofs)
      (visibility public)
      (source
       (path Principles_proofs)
       (intf (path plugin/principles_proofs.mli))
       (impl (path plugin/principles_proofs.ml))))
     (module
      (obj_name equations_plugin__Sigma_types)
      (visibility public)
      (source
       (path Sigma_types)
       (intf (path plugin/sigma_types.mli))
       (impl (path plugin/sigma_types.ml))))
     (module
      (obj_name equations_plugin__Simplify)
      (visibility public)
      (source
       (path Simplify)
       (intf (path plugin/simplify.mli))
       (impl (path plugin/simplify.ml))))
     (module
      (obj_name equations_plugin__Splitting)
      (visibility public)
      (source
       (path Splitting)
       (intf (path plugin/splitting.mli))
       (impl (path plugin/splitting.ml))))
     (module
      (obj_name equations_plugin__Subterm)
      (visibility public)
      (source
       (path Subterm)
       (intf (path plugin/subterm.mli))
       (impl (path plugin/subterm.ml))))
     (module
      (obj_name equations_plugin__Syntax)
      (visibility public)
      (source
       (path Syntax)
       (intf (path plugin/syntax.mli))
       (impl (path plugin/syntax.ml))))))
   (wrapped true))))
