(lang dune 3.17)
(name easycrypt)
(version 05c2a38)
(sections
 (lib /usr/lib/easycrypt)
 (lib_root /usr/lib)
 (libexec /usr/lib/easycrypt)
 (libexec_root /usr/lib)
 (bin /usr/bin)
 (doc /usr/doc/easycrypt)
 (stublibs /usr/lib/stublibs))
(sites (commands libexec) (config lib) (doc lib) (theories lib))
(files
 (lib
  (META
   dune-package
   ecLib/EcDuneSites.ml
   ecLib/ecAlgTactic.ml
   ecLib/ecAlgTactic.mli
   ecLib/ecAlgebra.ml
   ecLib/ecAlgebra.mli
   ecLib/ecAlphaInvHashtbl.ml
   ecLib/ecAlphaInvHashtbl.mli
   ecLib/ecAst.ml
   ecLib/ecAst.mli
   ecLib/ecBaseLogic.ml
   ecLib/ecBigInt.ml
   ecLib/ecBigInt.mli
   ecLib/ecBigIntCore.ml
   ecLib/ecBullets.ml
   ecLib/ecBullets.mli
   ecLib/ecCallbyValue.ml
   ecLib/ecCallbyValue.mli
   ecLib/ecCircuits.ml
   ecLib/ecCircuits.mli
   ecLib/ecCommands.ml
   ecLib/ecCommands.mli
   ecLib/ecCoq.ml
   ecLib/ecCoq.mli
   ecLib/ecCoreFol.ml
   ecLib/ecCoreFol.mli
   ecLib/ecCoreGoal.ml
   ecLib/ecCoreGoal.mli
   ecLib/ecCoreLib.ml
   ecLib/ecCoreLib.mli
   ecLib/ecCoreModules.ml
   ecLib/ecCoreModules.mli
   ecLib/ecCorePrinting.ml
   ecLib/ecCoreSubst.ml
   ecLib/ecCoreSubst.mli
   ecLib/ecDecl.ml
   ecLib/ecDecl.mli
   ecLib/ecDoc.ml
   ecLib/ecDoc.mli
   ecLib/ecEco.ml
   ecLib/ecEnv.ml
   ecLib/ecEnv.mli
   ecLib/ecField.ml
   ecLib/ecField.mli
   ecLib/ecFol.ml
   ecLib/ecFol.mli
   ecLib/ecGState.ml
   ecLib/ecGState.mli
   ecLib/ecGenRegexp.ml
   ecLib/ecHiGoal.ml
   ecLib/ecHiGoal.mli
   ecLib/ecHiInductive.ml
   ecLib/ecHiInductive.mli
   ecLib/ecHiNotations.ml
   ecLib/ecHiNotations.mli
   ecLib/ecHiPredicates.ml
   ecLib/ecHiPredicates.mli
   ecLib/ecHiTacticals.ml
   ecLib/ecHiTacticals.mli
   ecLib/ecIdent.ml
   ecLib/ecIdent.mli
   ecLib/ecInductive.ml
   ecLib/ecInductive.mli
   ecLib/ecIo.ml
   ecLib/ecIo.mli
   ecLib/ecLexer.ml
   ecLib/ecLib.a
   ecLib/ecLib.cma
   ecLib/ecLib.cmi
   ecLib/ecLib.cmt
   ecLib/ecLib.cmx
   ecLib/ecLib.cmxa
   ecLib/ecLib.ml
   ecLib/ecLib__EUnix.cmi
   ecLib/ecLib__EUnix.cmt
   ecLib/ecLib__EUnix.cmti
   ecLib/ecLib__EUnix.cmx
   ecLib/ecLib__EcAlgTactic.cmi
   ecLib/ecLib__EcAlgTactic.cmt
   ecLib/ecLib__EcAlgTactic.cmti
   ecLib/ecLib__EcAlgTactic.cmx
   ecLib/ecLib__EcAlgebra.cmi
   ecLib/ecLib__EcAlgebra.cmt
   ecLib/ecLib__EcAlgebra.cmti
   ecLib/ecLib__EcAlgebra.cmx
   ecLib/ecLib__EcAlphaInvHashtbl.cmi
   ecLib/ecLib__EcAlphaInvHashtbl.cmt
   ecLib/ecLib__EcAlphaInvHashtbl.cmti
   ecLib/ecLib__EcAlphaInvHashtbl.cmx
   ecLib/ecLib__EcAst.cmi
   ecLib/ecLib__EcAst.cmt
   ecLib/ecLib__EcAst.cmti
   ecLib/ecLib__EcAst.cmx
   ecLib/ecLib__EcBaseLogic.cmi
   ecLib/ecLib__EcBaseLogic.cmt
   ecLib/ecLib__EcBaseLogic.cmx
   ecLib/ecLib__EcBigInt.cmi
   ecLib/ecLib__EcBigInt.cmt
   ecLib/ecLib__EcBigInt.cmti
   ecLib/ecLib__EcBigInt.cmx
   ecLib/ecLib__EcBigIntCore.cmi
   ecLib/ecLib__EcBigIntCore.cmt
   ecLib/ecLib__EcBigIntCore.cmx
   ecLib/ecLib__EcBullets.cmi
   ecLib/ecLib__EcBullets.cmt
   ecLib/ecLib__EcBullets.cmti
   ecLib/ecLib__EcBullets.cmx
   ecLib/ecLib__EcCallbyValue.cmi
   ecLib/ecLib__EcCallbyValue.cmt
   ecLib/ecLib__EcCallbyValue.cmti
   ecLib/ecLib__EcCallbyValue.cmx
   ecLib/ecLib__EcCircuits.cmi
   ecLib/ecLib__EcCircuits.cmt
   ecLib/ecLib__EcCircuits.cmti
   ecLib/ecLib__EcCircuits.cmx
   ecLib/ecLib__EcCommands.cmi
   ecLib/ecLib__EcCommands.cmt
   ecLib/ecLib__EcCommands.cmti
   ecLib/ecLib__EcCommands.cmx
   ecLib/ecLib__EcCoq.cmi
   ecLib/ecLib__EcCoq.cmt
   ecLib/ecLib__EcCoq.cmti
   ecLib/ecLib__EcCoq.cmx
   ecLib/ecLib__EcCoreFol.cmi
   ecLib/ecLib__EcCoreFol.cmt
   ecLib/ecLib__EcCoreFol.cmti
   ecLib/ecLib__EcCoreFol.cmx
   ecLib/ecLib__EcCoreGoal.cmi
   ecLib/ecLib__EcCoreGoal.cmt
   ecLib/ecLib__EcCoreGoal.cmti
   ecLib/ecLib__EcCoreGoal.cmx
   ecLib/ecLib__EcCoreLib.cmi
   ecLib/ecLib__EcCoreLib.cmt
   ecLib/ecLib__EcCoreLib.cmti
   ecLib/ecLib__EcCoreLib.cmx
   ecLib/ecLib__EcCoreModules.cmi
   ecLib/ecLib__EcCoreModules.cmt
   ecLib/ecLib__EcCoreModules.cmti
   ecLib/ecLib__EcCoreModules.cmx
   ecLib/ecLib__EcCorePrinting.cmi
   ecLib/ecLib__EcCorePrinting.cmt
   ecLib/ecLib__EcCorePrinting.cmx
   ecLib/ecLib__EcCoreSubst.cmi
   ecLib/ecLib__EcCoreSubst.cmt
   ecLib/ecLib__EcCoreSubst.cmti
   ecLib/ecLib__EcCoreSubst.cmx
   ecLib/ecLib__EcDecl.cmi
   ecLib/ecLib__EcDecl.cmt
   ecLib/ecLib__EcDecl.cmti
   ecLib/ecLib__EcDecl.cmx
   ecLib/ecLib__EcDoc.cmi
   ecLib/ecLib__EcDoc.cmt
   ecLib/ecLib__EcDoc.cmti
   ecLib/ecLib__EcDoc.cmx
   ecLib/ecLib__EcDuneSites.cmi
   ecLib/ecLib__EcDuneSites.cmt
   ecLib/ecLib__EcDuneSites.cmx
   ecLib/ecLib__EcEco.cmi
   ecLib/ecLib__EcEco.cmt
   ecLib/ecLib__EcEco.cmx
   ecLib/ecLib__EcEnv.cmi
   ecLib/ecLib__EcEnv.cmt
   ecLib/ecLib__EcEnv.cmti
   ecLib/ecLib__EcEnv.cmx
   ecLib/ecLib__EcField.cmi
   ecLib/ecLib__EcField.cmt
   ecLib/ecLib__EcField.cmti
   ecLib/ecLib__EcField.cmx
   ecLib/ecLib__EcFol.cmi
   ecLib/ecLib__EcFol.cmt
   ecLib/ecLib__EcFol.cmti
   ecLib/ecLib__EcFol.cmx
   ecLib/ecLib__EcGState.cmi
   ecLib/ecLib__EcGState.cmt
   ecLib/ecLib__EcGState.cmti
   ecLib/ecLib__EcGState.cmx
   ecLib/ecLib__EcGenRegexp.cmi
   ecLib/ecLib__EcGenRegexp.cmt
   ecLib/ecLib__EcGenRegexp.cmx
   ecLib/ecLib__EcHiGoal.cmi
   ecLib/ecLib__EcHiGoal.cmt
   ecLib/ecLib__EcHiGoal.cmti
   ecLib/ecLib__EcHiGoal.cmx
   ecLib/ecLib__EcHiInductive.cmi
   ecLib/ecLib__EcHiInductive.cmt
   ecLib/ecLib__EcHiInductive.cmti
   ecLib/ecLib__EcHiInductive.cmx
   ecLib/ecLib__EcHiNotations.cmi
   ecLib/ecLib__EcHiNotations.cmt
   ecLib/ecLib__EcHiNotations.cmti
   ecLib/ecLib__EcHiNotations.cmx
   ecLib/ecLib__EcHiPredicates.cmi
   ecLib/ecLib__EcHiPredicates.cmt
   ecLib/ecLib__EcHiPredicates.cmti
   ecLib/ecLib__EcHiPredicates.cmx
   ecLib/ecLib__EcHiTacticals.cmi
   ecLib/ecLib__EcHiTacticals.cmt
   ecLib/ecLib__EcHiTacticals.cmti
   ecLib/ecLib__EcHiTacticals.cmx
   ecLib/ecLib__EcIdent.cmi
   ecLib/ecLib__EcIdent.cmt
   ecLib/ecLib__EcIdent.cmti
   ecLib/ecLib__EcIdent.cmx
   ecLib/ecLib__EcInductive.cmi
   ecLib/ecLib__EcInductive.cmt
   ecLib/ecLib__EcInductive.cmti
   ecLib/ecLib__EcInductive.cmx
   ecLib/ecLib__EcIo.cmi
   ecLib/ecLib__EcIo.cmt
   ecLib/ecLib__EcIo.cmti
   ecLib/ecLib__EcIo.cmx
   ecLib/ecLib__EcLexer.cmi
   ecLib/ecLib__EcLexer.cmt
   ecLib/ecLib__EcLexer.cmx
   ecLib/ecLib__EcLoader.cmi
   ecLib/ecLib__EcLoader.cmt
   ecLib/ecLib__EcLoader.cmti
   ecLib/ecLib__EcLoader.cmx
   ecLib/ecLib__EcLocation.cmi
   ecLib/ecLib__EcLocation.cmt
   ecLib/ecLib__EcLocation.cmti
   ecLib/ecLib__EcLocation.cmx
   ecLib/ecLib__EcLowCircuits.cmi
   ecLib/ecLib__EcLowCircuits.cmt
   ecLib/ecLib__EcLowCircuits.cmti
   ecLib/ecLib__EcLowCircuits.cmx
   ecLib/ecLib__EcLowGoal.cmi
   ecLib/ecLib__EcLowGoal.cmt
   ecLib/ecLib__EcLowGoal.cmti
   ecLib/ecLib__EcLowGoal.cmx
   ecLib/ecLib__EcLowPhlGoal.cmi
   ecLib/ecLib__EcLowPhlGoal.cmt
   ecLib/ecLib__EcLowPhlGoal.cmx
   ecLib/ecLib__EcMaps.cmi
   ecLib/ecLib__EcMaps.cmt
   ecLib/ecLib__EcMaps.cmx
   ecLib/ecLib__EcMatching.cmi
   ecLib/ecLib__EcMatching.cmt
   ecLib/ecLib__EcMatching.cmti
   ecLib/ecLib__EcMatching.cmx
   ecLib/ecLib__EcMemory.cmi
   ecLib/ecLib__EcMemory.cmt
   ecLib/ecLib__EcMemory.cmti
   ecLib/ecLib__EcMemory.cmx
   ecLib/ecLib__EcModules.cmi
   ecLib/ecLib__EcModules.cmt
   ecLib/ecLib__EcModules.cmti
   ecLib/ecLib__EcModules.cmx
   ecLib/ecLib__EcOptions.cmi
   ecLib/ecLib__EcOptions.cmt
   ecLib/ecLib__EcOptions.cmti
   ecLib/ecLib__EcOptions.cmx
   ecLib/ecLib__EcPException.cmi
   ecLib/ecLib__EcPException.cmt
   ecLib/ecLib__EcPException.cmti
   ecLib/ecLib__EcPException.cmx
   ecLib/ecLib__EcPV.cmi
   ecLib/ecLib__EcPV.cmt
   ecLib/ecLib__EcPV.cmti
   ecLib/ecLib__EcPV.cmx
   ecLib/ecLib__EcParser.cmi
   ecLib/ecLib__EcParser.cmt
   ecLib/ecLib__EcParser.cmti
   ecLib/ecLib__EcParser.cmx
   ecLib/ecLib__EcParsetree.cmi
   ecLib/ecLib__EcParsetree.cmt
   ecLib/ecLib__EcParsetree.cmx
   ecLib/ecLib__EcPath.cmi
   ecLib/ecLib__EcPath.cmt
   ecLib/ecLib__EcPath.cmti
   ecLib/ecLib__EcPath.cmx
   ecLib/ecLib__EcPhlAuto.cmi
   ecLib/ecLib__EcPhlAuto.cmt
   ecLib/ecLib__EcPhlAuto.cmti
   ecLib/ecLib__EcPhlAuto.cmx
   ecLib/ecLib__EcPhlBDep.cmi
   ecLib/ecLib__EcPhlBDep.cmt
   ecLib/ecLib__EcPhlBDep.cmti
   ecLib/ecLib__EcPhlBDep.cmx
   ecLib/ecLib__EcPhlBdHoare.cmi
   ecLib/ecLib__EcPhlBdHoare.cmt
   ecLib/ecLib__EcPhlBdHoare.cmti
   ecLib/ecLib__EcPhlBdHoare.cmx
   ecLib/ecLib__EcPhlCall.cmi
   ecLib/ecLib__EcPhlCall.cmt
   ecLib/ecLib__EcPhlCall.cmti
   ecLib/ecLib__EcPhlCall.cmx
   ecLib/ecLib__EcPhlCase.cmi
   ecLib/ecLib__EcPhlCase.cmt
   ecLib/ecLib__EcPhlCase.cmti
   ecLib/ecLib__EcPhlCase.cmx
   ecLib/ecLib__EcPhlCodeTx.cmi
   ecLib/ecLib__EcPhlCodeTx.cmt
   ecLib/ecLib__EcPhlCodeTx.cmti
   ecLib/ecLib__EcPhlCodeTx.cmx
   ecLib/ecLib__EcPhlCond.cmi
   ecLib/ecLib__EcPhlCond.cmt
   ecLib/ecLib__EcPhlCond.cmti
   ecLib/ecLib__EcPhlCond.cmx
   ecLib/ecLib__EcPhlConseq.cmi
   ecLib/ecLib__EcPhlConseq.cmt
   ecLib/ecLib__EcPhlConseq.cmti
   ecLib/ecLib__EcPhlConseq.cmx
   ecLib/ecLib__EcPhlCoreView.cmi
   ecLib/ecLib__EcPhlCoreView.cmt
   ecLib/ecLib__EcPhlCoreView.cmti
   ecLib/ecLib__EcPhlCoreView.cmx
   ecLib/ecLib__EcPhlDeno.cmi
   ecLib/ecLib__EcPhlDeno.cmt
   ecLib/ecLib__EcPhlDeno.cmti
   ecLib/ecLib__EcPhlDeno.cmx
   ecLib/ecLib__EcPhlEager.cmi
   ecLib/ecLib__EcPhlEager.cmt
   ecLib/ecLib__EcPhlEager.cmti
   ecLib/ecLib__EcPhlEager.cmx
   ecLib/ecLib__EcPhlEqobs.cmi
   ecLib/ecLib__EcPhlEqobs.cmt
   ecLib/ecLib__EcPhlEqobs.cmti
   ecLib/ecLib__EcPhlEqobs.cmx
   ecLib/ecLib__EcPhlExists.cmi
   ecLib/ecLib__EcPhlExists.cmt
   ecLib/ecLib__EcPhlExists.cmti
   ecLib/ecLib__EcPhlExists.cmx
   ecLib/ecLib__EcPhlFel.cmi
   ecLib/ecLib__EcPhlFel.cmt
   ecLib/ecLib__EcPhlFel.cmti
   ecLib/ecLib__EcPhlFel.cmx
   ecLib/ecLib__EcPhlFun.cmi
   ecLib/ecLib__EcPhlFun.cmt
   ecLib/ecLib__EcPhlFun.cmti
   ecLib/ecLib__EcPhlFun.cmx
   ecLib/ecLib__EcPhlHiAuto.cmi
   ecLib/ecLib__EcPhlHiAuto.cmt
   ecLib/ecLib__EcPhlHiAuto.cmti
   ecLib/ecLib__EcPhlHiAuto.cmx
   ecLib/ecLib__EcPhlHiBdHoare.cmi
   ecLib/ecLib__EcPhlHiBdHoare.cmt
   ecLib/ecLib__EcPhlHiBdHoare.cmti
   ecLib/ecLib__EcPhlHiBdHoare.cmx
   ecLib/ecLib__EcPhlHiCond.cmi
   ecLib/ecLib__EcPhlHiCond.cmt
   ecLib/ecLib__EcPhlHiCond.cmti
   ecLib/ecLib__EcPhlHiCond.cmx
   ecLib/ecLib__EcPhlHoare.cmi
   ecLib/ecLib__EcPhlHoare.cmt
   ecLib/ecLib__EcPhlHoare.cmti
   ecLib/ecLib__EcPhlHoare.cmx
   ecLib/ecLib__EcPhlInline.cmi
   ecLib/ecLib__EcPhlInline.cmt
   ecLib/ecLib__EcPhlInline.cmti
   ecLib/ecLib__EcPhlInline.cmx
   ecLib/ecLib__EcPhlLoopTx.cmi
   ecLib/ecLib__EcPhlLoopTx.cmt
   ecLib/ecLib__EcPhlLoopTx.cmti
   ecLib/ecLib__EcPhlLoopTx.cmx
   ecLib/ecLib__EcPhlOutline.cmi
   ecLib/ecLib__EcPhlOutline.cmt
   ecLib/ecLib__EcPhlOutline.cmti
   ecLib/ecLib__EcPhlOutline.cmx
   ecLib/ecLib__EcPhlPr.cmi
   ecLib/ecLib__EcPhlPr.cmt
   ecLib/ecLib__EcPhlPr.cmti
   ecLib/ecLib__EcPhlPr.cmx
   ecLib/ecLib__EcPhlPrRw.cmi
   ecLib/ecLib__EcPhlPrRw.cmt
   ecLib/ecLib__EcPhlPrRw.cmti
   ecLib/ecLib__EcPhlPrRw.cmx
   ecLib/ecLib__EcPhlRCond.cmi
   ecLib/ecLib__EcPhlRCond.cmt
   ecLib/ecLib__EcPhlRCond.cmti
   ecLib/ecLib__EcPhlRCond.cmx
   ecLib/ecLib__EcPhlRewrite.cmi
   ecLib/ecLib__EcPhlRewrite.cmt
   ecLib/ecLib__EcPhlRewrite.cmti
   ecLib/ecLib__EcPhlRewrite.cmx
   ecLib/ecLib__EcPhlRnd.cmi
   ecLib/ecLib__EcPhlRnd.cmt
   ecLib/ecLib__EcPhlRnd.cmti
   ecLib/ecLib__EcPhlRnd.cmx
   ecLib/ecLib__EcPhlRwEquiv.cmi
   ecLib/ecLib__EcPhlRwEquiv.cmt
   ecLib/ecLib__EcPhlRwEquiv.cmti
   ecLib/ecLib__EcPhlRwEquiv.cmx
   ecLib/ecLib__EcPhlRwPrgm.cmi
   ecLib/ecLib__EcPhlRwPrgm.cmt
   ecLib/ecLib__EcPhlRwPrgm.cmx
   ecLib/ecLib__EcPhlSeq.cmi
   ecLib/ecLib__EcPhlSeq.cmt
   ecLib/ecLib__EcPhlSeq.cmti
   ecLib/ecLib__EcPhlSeq.cmx
   ecLib/ecLib__EcPhlSkip.cmi
   ecLib/ecLib__EcPhlSkip.cmt
   ecLib/ecLib__EcPhlSkip.cmti
   ecLib/ecLib__EcPhlSkip.cmx
   ecLib/ecLib__EcPhlSp.cmi
   ecLib/ecLib__EcPhlSp.cmt
   ecLib/ecLib__EcPhlSp.cmti
   ecLib/ecLib__EcPhlSp.cmx
   ecLib/ecLib__EcPhlSwap.cmi
   ecLib/ecLib__EcPhlSwap.cmt
   ecLib/ecLib__EcPhlSwap.cmti
   ecLib/ecLib__EcPhlSwap.cmx
   ecLib/ecLib__EcPhlSym.cmi
   ecLib/ecLib__EcPhlSym.cmt
   ecLib/ecLib__EcPhlSym.cmti
   ecLib/ecLib__EcPhlSym.cmx
   ecLib/ecLib__EcPhlTAuto.cmi
   ecLib/ecLib__EcPhlTAuto.cmt
   ecLib/ecLib__EcPhlTAuto.cmti
   ecLib/ecLib__EcPhlTAuto.cmx
   ecLib/ecLib__EcPhlTrans.cmi
   ecLib/ecLib__EcPhlTrans.cmt
   ecLib/ecLib__EcPhlTrans.cmti
   ecLib/ecLib__EcPhlTrans.cmx
   ecLib/ecLib__EcPhlUpto.cmi
   ecLib/ecLib__EcPhlUpto.cmt
   ecLib/ecLib__EcPhlUpto.cmti
   ecLib/ecLib__EcPhlUpto.cmx
   ecLib/ecLib__EcPhlWhile.cmi
   ecLib/ecLib__EcPhlWhile.cmt
   ecLib/ecLib__EcPhlWhile.cmti
   ecLib/ecLib__EcPhlWhile.cmx
   ecLib/ecLib__EcPhlWp.cmi
   ecLib/ecLib__EcPhlWp.cmt
   ecLib/ecLib__EcPhlWp.cmti
   ecLib/ecLib__EcPhlWp.cmx
   ecLib/ecLib__EcPrinting.cmi
   ecLib/ecLib__EcPrinting.cmt
   ecLib/ecLib__EcPrinting.cmti
   ecLib/ecLib__EcPrinting.cmx
   ecLib/ecLib__EcProcSem.cmi
   ecLib/ecLib__EcProcSem.cmt
   ecLib/ecLib__EcProcSem.cmti
   ecLib/ecLib__EcProcSem.cmx
   ecLib/ecLib__EcProofTerm.cmi
   ecLib/ecLib__EcProofTerm.cmt
   ecLib/ecLib__EcProofTerm.cmti
   ecLib/ecLib__EcProofTerm.cmx
   ecLib/ecLib__EcProofTyping.cmi
   ecLib/ecLib__EcProofTyping.cmt
   ecLib/ecLib__EcProofTyping.cmti
   ecLib/ecLib__EcProofTyping.cmx
   ecLib/ecLib__EcProvers.cmi
   ecLib/ecLib__EcProvers.cmt
   ecLib/ecLib__EcProvers.cmti
   ecLib/ecLib__EcProvers.cmx
   ecLib/ecLib__EcReduction.cmi
   ecLib/ecLib__EcReduction.cmt
   ecLib/ecLib__EcReduction.cmti
   ecLib/ecLib__EcReduction.cmx
   ecLib/ecLib__EcRegexp.cmi
   ecLib/ecLib__EcRegexp.cmt
   ecLib/ecLib__EcRegexp.cmti
   ecLib/ecLib__EcRegexp.cmx
   ecLib/ecLib__EcRelocate.cmi
   ecLib/ecLib__EcRelocate.cmt
   ecLib/ecLib__EcRelocate.cmti
   ecLib/ecLib__EcRelocate.cmx
   ecLib/ecLib__EcRing.cmi
   ecLib/ecLib__EcRing.cmt
   ecLib/ecLib__EcRing.cmti
   ecLib/ecLib__EcRing.cmx
   ecLib/ecLib__EcScope.cmi
   ecLib/ecLib__EcScope.cmt
   ecLib/ecLib__EcScope.cmti
   ecLib/ecLib__EcScope.cmx
   ecLib/ecLib__EcSearch.cmi
   ecLib/ecLib__EcSearch.cmt
   ecLib/ecLib__EcSearch.cmti
   ecLib/ecLib__EcSearch.cmx
   ecLib/ecLib__EcSection.cmi
   ecLib/ecLib__EcSection.cmt
   ecLib/ecLib__EcSection.cmti
   ecLib/ecLib__EcSection.cmx
   ecLib/ecLib__EcSimplifyContext.cmi
   ecLib/ecLib__EcSimplifyContext.cmt
   ecLib/ecLib__EcSimplifyContext.cmti
   ecLib/ecLib__EcSimplifyContext.cmx
   ecLib/ecLib__EcSmt.cmi
   ecLib/ecLib__EcSmt.cmt
   ecLib/ecLib__EcSmt.cmti
   ecLib/ecLib__EcSmt.cmx
   ecLib/ecLib__EcStrongRing.cmi
   ecLib/ecLib__EcStrongRing.cmt
   ecLib/ecLib__EcStrongRing.cmx
   ecLib/ecLib__EcSubst.cmi
   ecLib/ecLib__EcSubst.cmt
   ecLib/ecLib__EcSubst.cmti
   ecLib/ecLib__EcSubst.cmx
   ecLib/ecLib__EcSymbols.cmi
   ecLib/ecLib__EcSymbols.cmt
   ecLib/ecLib__EcSymbols.cmti
   ecLib/ecLib__EcSymbols.cmx
   ecLib/ecLib__EcTerminal.cmi
   ecLib/ecLib__EcTerminal.cmt
   ecLib/ecLib__EcTerminal.cmti
   ecLib/ecLib__EcTerminal.cmx
   ecLib/ecLib__EcThCloning.cmi
   ecLib/ecLib__EcThCloning.cmt
   ecLib/ecLib__EcThCloning.cmti
   ecLib/ecLib__EcThCloning.cmx
   ecLib/ecLib__EcTheory.cmi
   ecLib/ecLib__EcTheory.cmt
   ecLib/ecLib__EcTheory.cmti
   ecLib/ecLib__EcTheory.cmx
   ecLib/ecLib__EcTheoryReplay.cmi
   ecLib/ecLib__EcTheoryReplay.cmt
   ecLib/ecLib__EcTheoryReplay.cmti
   ecLib/ecLib__EcTheoryReplay.cmx
   ecLib/ecLib__EcTransMatching.cmi
   ecLib/ecLib__EcTransMatching.cmt
   ecLib/ecLib__EcTransMatching.cmti
   ecLib/ecLib__EcTransMatching.cmx
   ecLib/ecLib__EcTypeClass.cmi
   ecLib/ecLib__EcTypeClass.cmt
   ecLib/ecLib__EcTypeClass.cmti
   ecLib/ecLib__EcTypeClass.cmx
   ecLib/ecLib__EcTypes.cmi
   ecLib/ecLib__EcTypes.cmt
   ecLib/ecLib__EcTypes.cmti
   ecLib/ecLib__EcTypes.cmx
   ecLib/ecLib__EcTypesafeFol.cmi
   ecLib/ecLib__EcTypesafeFol.cmt
   ecLib/ecLib__EcTypesafeFol.cmti
   ecLib/ecLib__EcTypesafeFol.cmx
   ecLib/ecLib__EcTyping.cmi
   ecLib/ecLib__EcTyping.cmt
   ecLib/ecLib__EcTyping.cmti
   ecLib/ecLib__EcTyping.cmx
   ecLib/ecLib__EcUFind.cmi
   ecLib/ecLib__EcUFind.cmt
   ecLib/ecLib__EcUFind.cmti
   ecLib/ecLib__EcUFind.cmx
   ecLib/ecLib__EcUid.cmi
   ecLib/ecLib__EcUid.cmt
   ecLib/ecLib__EcUid.cmti
   ecLib/ecLib__EcUid.cmx
   ecLib/ecLib__EcUnify.cmi
   ecLib/ecLib__EcUnify.cmt
   ecLib/ecLib__EcUnify.cmti
   ecLib/ecLib__EcUnify.cmx
   ecLib/ecLib__EcUnifyProc.cmi
   ecLib/ecLib__EcUnifyProc.cmt
   ecLib/ecLib__EcUnifyProc.cmti
   ecLib/ecLib__EcUnifyProc.cmx
   ecLib/ecLib__EcUserMessages.cmi
   ecLib/ecLib__EcUserMessages.cmt
   ecLib/ecLib__EcUserMessages.cmti
   ecLib/ecLib__EcUserMessages.cmx
   ecLib/ecLib__EcUtils.cmi
   ecLib/ecLib__EcUtils.cmt
   ecLib/ecLib__EcUtils.cmti
   ecLib/ecLib__EcUtils.cmx
   ecLib/ecLib__EcVersion.cmi
   ecLib/ecLib__EcVersion.cmt
   ecLib/ecLib__EcVersion.cmti
   ecLib/ecLib__EcVersion.cmx
   ecLib/ecLib__EcWhy3Conv.cmi
   ecLib/ecLib__EcWhy3Conv.cmt
   ecLib/ecLib__EcWhy3Conv.cmti
   ecLib/ecLib__EcWhy3Conv.cmx
   ecLib/ecLib__XDG.cmi
   ecLib/ecLib__XDG.cmt
   ecLib/ecLib__XDG.cmti
   ecLib/ecLib__XDG.cmx
   ecLib/ecLoader.ml
   ecLib/ecLoader.mli
   ecLib/ecLocation.ml
   ecLib/ecLocation.mli
   ecLib/ecLowCircuits.ml
   ecLib/ecLowCircuits.mli
   ecLib/ecLowGoal.ml
   ecLib/ecLowGoal.mli
   ecLib/ecLowPhlGoal.ml
   ecLib/ecMaps.ml
   ecLib/ecMatching.ml
   ecLib/ecMatching.mli
   ecLib/ecMemory.ml
   ecLib/ecMemory.mli
   ecLib/ecModules.ml
   ecLib/ecModules.mli
   ecLib/ecOptions.ml
   ecLib/ecOptions.mli
   ecLib/ecPException.ml
   ecLib/ecPException.mli
   ecLib/ecPV.ml
   ecLib/ecPV.mli
   ecLib/ecParser.ml
   ecLib/ecParser.mli
   ecLib/ecParsetree.ml
   ecLib/ecPath.ml
   ecLib/ecPath.mli
   ecLib/ecPrinting.ml
   ecLib/ecPrinting.mli
   ecLib/ecProcSem.ml
   ecLib/ecProcSem.mli
   ecLib/ecProofTerm.ml
   ecLib/ecProofTerm.mli
   ecLib/ecProofTyping.ml
   ecLib/ecProofTyping.mli
   ecLib/ecProvers.ml
   ecLib/ecProvers.mli
   ecLib/ecReduction.ml
   ecLib/ecReduction.mli
   ecLib/ecRegexp.ml
   ecLib/ecRegexp.mli
   ecLib/ecRelocate.ml
   ecLib/ecRelocate.mli
   ecLib/ecRing.ml
   ecLib/ecRing.mli
   ecLib/ecScope.ml
   ecLib/ecScope.mli
   ecLib/ecSearch.ml
   ecLib/ecSearch.mli
   ecLib/ecSection.ml
   ecLib/ecSection.mli
   ecLib/ecSimplifyContext.ml
   ecLib/ecSimplifyContext.mli
   ecLib/ecSmt.ml
   ecLib/ecSmt.mli
   ecLib/ecStrongRing.ml
   ecLib/ecSubst.ml
   ecLib/ecSubst.mli
   ecLib/ecSymbols.ml
   ecLib/ecSymbols.mli
   ecLib/ecTerminal.ml
   ecLib/ecTerminal.mli
   ecLib/ecThCloning.ml
   ecLib/ecThCloning.mli
   ecLib/ecTheory.ml
   ecLib/ecTheory.mli
   ecLib/ecTheoryReplay.ml
   ecLib/ecTheoryReplay.mli
   ecLib/ecTransMatching.ml
   ecLib/ecTransMatching.mli
   ecLib/ecTypeClass.ml
   ecLib/ecTypeClass.mli
   ecLib/ecTypes.ml
   ecLib/ecTypes.mli
   ecLib/ecTypesafeFol.ml
   ecLib/ecTypesafeFol.mli
   ecLib/ecTyping.ml
   ecLib/ecTyping.mli
   ecLib/ecUFind.ml
   ecLib/ecUFind.mli
   ecLib/ecUid.ml
   ecLib/ecUid.mli
   ecLib/ecUnify.ml
   ecLib/ecUnify.mli
   ecLib/ecUnifyProc.ml
   ecLib/ecUnifyProc.mli
   ecLib/ecUserMessages.ml
   ecLib/ecUserMessages.mli
   ecLib/ecUtils.ml
   ecLib/ecUtils.mli
   ecLib/ecVersion.ml
   ecLib/ecVersion.mli
   ecLib/ecWhy3Conv.ml
   ecLib/ecWhy3Conv.mli
   ecLib/libecLib_stubs.a
   ecLib/phl/ecPhlAuto.ml
   ecLib/phl/ecPhlAuto.mli
   ecLib/phl/ecPhlBDep.ml
   ecLib/phl/ecPhlBDep.mli
   ecLib/phl/ecPhlBdHoare.ml
   ecLib/phl/ecPhlBdHoare.mli
   ecLib/phl/ecPhlCall.ml
   ecLib/phl/ecPhlCall.mli
   ecLib/phl/ecPhlCase.ml
   ecLib/phl/ecPhlCase.mli
   ecLib/phl/ecPhlCodeTx.ml
   ecLib/phl/ecPhlCodeTx.mli
   ecLib/phl/ecPhlCond.ml
   ecLib/phl/ecPhlCond.mli
   ecLib/phl/ecPhlConseq.ml
   ecLib/phl/ecPhlConseq.mli
   ecLib/phl/ecPhlCoreView.ml
   ecLib/phl/ecPhlCoreView.mli
   ecLib/phl/ecPhlDeno.ml
   ecLib/phl/ecPhlDeno.mli
   ecLib/phl/ecPhlEager.ml
   ecLib/phl/ecPhlEager.mli
   ecLib/phl/ecPhlEqobs.ml
   ecLib/phl/ecPhlEqobs.mli
   ecLib/phl/ecPhlExists.ml
   ecLib/phl/ecPhlExists.mli
   ecLib/phl/ecPhlFel.ml
   ecLib/phl/ecPhlFel.mli
   ecLib/phl/ecPhlFun.ml
   ecLib/phl/ecPhlFun.mli
   ecLib/phl/ecPhlHiAuto.ml
   ecLib/phl/ecPhlHiAuto.mli
   ecLib/phl/ecPhlHiBdHoare.ml
   ecLib/phl/ecPhlHiBdHoare.mli
   ecLib/phl/ecPhlHiCond.ml
   ecLib/phl/ecPhlHiCond.mli
   ecLib/phl/ecPhlHoare.ml
   ecLib/phl/ecPhlHoare.mli
   ecLib/phl/ecPhlInline.ml
   ecLib/phl/ecPhlInline.mli
   ecLib/phl/ecPhlLoopTx.ml
   ecLib/phl/ecPhlLoopTx.mli
   ecLib/phl/ecPhlOutline.ml
   ecLib/phl/ecPhlOutline.mli
   ecLib/phl/ecPhlPr.ml
   ecLib/phl/ecPhlPr.mli
   ecLib/phl/ecPhlPrRw.ml
   ecLib/phl/ecPhlPrRw.mli
   ecLib/phl/ecPhlRCond.ml
   ecLib/phl/ecPhlRCond.mli
   ecLib/phl/ecPhlRewrite.ml
   ecLib/phl/ecPhlRewrite.mli
   ecLib/phl/ecPhlRnd.ml
   ecLib/phl/ecPhlRnd.mli
   ecLib/phl/ecPhlRwEquiv.ml
   ecLib/phl/ecPhlRwEquiv.mli
   ecLib/phl/ecPhlRwPrgm.ml
   ecLib/phl/ecPhlSeq.ml
   ecLib/phl/ecPhlSeq.mli
   ecLib/phl/ecPhlSkip.ml
   ecLib/phl/ecPhlSkip.mli
   ecLib/phl/ecPhlSp.ml
   ecLib/phl/ecPhlSp.mli
   ecLib/phl/ecPhlSwap.ml
   ecLib/phl/ecPhlSwap.mli
   ecLib/phl/ecPhlSym.ml
   ecLib/phl/ecPhlSym.mli
   ecLib/phl/ecPhlTAuto.ml
   ecLib/phl/ecPhlTAuto.mli
   ecLib/phl/ecPhlTrans.ml
   ecLib/phl/ecPhlTrans.mli
   ecLib/phl/ecPhlUpto.ml
   ecLib/phl/ecPhlUpto.mli
   ecLib/phl/ecPhlWhile.ml
   ecLib/phl/ecPhlWhile.mli
   ecLib/phl/ecPhlWp.ml
   ecLib/phl/ecPhlWp.mli
   ecLib/system/EUnix.ml
   ecLib/system/EUnix.mli
   ecLib/system/XDG.ml
   ecLib/system/XDG.mli
   inifiles/inifiles.a
   inifiles/inifiles.cma
   inifiles/inifiles.cmi
   inifiles/inifiles.cmt
   inifiles/inifiles.cmti
   inifiles/inifiles.cmx
   inifiles/inifiles.cmxa
   inifiles/inifiles.ml
   inifiles/inifiles.mli
   inifiles/inifiles__.cmi
   inifiles/inifiles__.cmt
   inifiles/inifiles__.cmx
   inifiles/inifiles__.ml
   inifiles/inifiles__Inilexer.cmi
   inifiles/inifiles__Inilexer.cmt
   inifiles/inifiles__Inilexer.cmx
   inifiles/inifiles__Parseini.cmi
   inifiles/inifiles__Parseini.cmt
   inifiles/inifiles__Parseini.cmti
   inifiles/inifiles__Parseini.cmx
   inifiles/inilexer.ml
   inifiles/parseini.ml
   inifiles/parseini.mli
   lospecs/aig.ml
   lospecs/aig.mli
   lospecs/ast.ml
   lospecs/ast.mli
   lospecs/circuit.ml
   lospecs/circuit.mli
   lospecs/deps.ml
   lospecs/deps.mli
   lospecs/io.ml
   lospecs/io.mli
   lospecs/lexer.ml
   lospecs/lospecs.a
   lospecs/lospecs.cma
   lospecs/lospecs.cmi
   lospecs/lospecs.cmt
   lospecs/lospecs.cmx
   lospecs/lospecs.cmxa
   lospecs/lospecs.ml
   lospecs/lospecs__Aig.cmi
   lospecs/lospecs__Aig.cmt
   lospecs/lospecs__Aig.cmti
   lospecs/lospecs__Aig.cmx
   lospecs/lospecs__Ast.cmi
   lospecs/lospecs__Ast.cmt
   lospecs/lospecs__Ast.cmti
   lospecs/lospecs__Ast.cmx
   lospecs/lospecs__Circuit.cmi
   lospecs/lospecs__Circuit.cmt
   lospecs/lospecs__Circuit.cmti
   lospecs/lospecs__Circuit.cmx
   lospecs/lospecs__Deps.cmi
   lospecs/lospecs__Deps.cmt
   lospecs/lospecs__Deps.cmti
   lospecs/lospecs__Deps.cmx
   lospecs/lospecs__Io.cmi
   lospecs/lospecs__Io.cmt
   lospecs/lospecs__Io.cmti
   lospecs/lospecs__Io.cmx
   lospecs/lospecs__Lexer.cmi
   lospecs/lospecs__Lexer.cmt
   lospecs/lospecs__Lexer.cmx
   lospecs/lospecs__Parser.cmi
   lospecs/lospecs__Parser.cmt
   lospecs/lospecs__Parser.cmti
   lospecs/lospecs__Parser.cmx
   lospecs/lospecs__Ptree.cmi
   lospecs/lospecs__Ptree.cmt
   lospecs/lospecs__Ptree.cmti
   lospecs/lospecs__Ptree.cmx
   lospecs/lospecs__Smt.cmi
   lospecs/lospecs__Smt.cmt
   lospecs/lospecs__Smt.cmti
   lospecs/lospecs__Smt.cmx
   lospecs/lospecs__Specifications.cmi
   lospecs/lospecs__Specifications.cmt
   lospecs/lospecs__Specifications.cmti
   lospecs/lospecs__Specifications.cmx
   lospecs/lospecs__Typing.cmi
   lospecs/lospecs__Typing.cmt
   lospecs/lospecs__Typing.cmti
   lospecs/lospecs__Typing.cmx
   lospecs/parser.ml
   lospecs/parser.mli
   lospecs/ptree.ml
   lospecs/ptree.mli
   lospecs/smt.ml
   lospecs/smt.mli
   lospecs/specifications.ml
   lospecs/specifications.mli
   lospecs/typing.ml
   lospecs/typing.mli
   opam))
 (lib_root
  (easycrypt/config/README
   easycrypt/doc/llm-guide.md
   easycrypt/doc/styles.css
   easycrypt/theories/algebra/Bigalg.ec
   easycrypt/theories/algebra/Bigop.eca
   easycrypt/theories/algebra/Binomial.ec
   easycrypt/theories/algebra/DynMatrix.eca
   easycrypt/theories/algebra/Group.ec
   easycrypt/theories/algebra/Ideal.ec
   easycrypt/theories/algebra/IntDiv.ec
   easycrypt/theories/algebra/Matrix.eca
   easycrypt/theories/algebra/Monoid.eca
   easycrypt/theories/algebra/Number.ec
   easycrypt/theories/algebra/Perms.ec
   easycrypt/theories/algebra/Poly.ec
   easycrypt/theories/algebra/PolyReduce.ec
   easycrypt/theories/algebra/Ring.ec
   easycrypt/theories/algebra/StdBigop.ec
   easycrypt/theories/algebra/StdOrder.ec
   easycrypt/theories/algebra/StdRing.ec
   easycrypt/theories/algebra/ZModP.ec
   easycrypt/theories/analysis/RealExp.ec
   easycrypt/theories/analysis/RealFLub.ec
   easycrypt/theories/analysis/RealFun.ec
   easycrypt/theories/analysis/RealLub.ec
   easycrypt/theories/analysis/RealSeq.ec
   easycrypt/theories/analysis/RealSeries.ec
   easycrypt/theories/core/AllCore.ec
   easycrypt/theories/core/Bool.ec
   easycrypt/theories/core/Core.ec
   easycrypt/theories/core/CoreInt.ec
   easycrypt/theories/core/CoreMap.ec
   easycrypt/theories/core/CoreReal.ec
   easycrypt/theories/crypto/AdvAbsVal.ec
   easycrypt/theories/crypto/Birthday.eca
   easycrypt/theories/crypto/Commitment.ec
   easycrypt/theories/crypto/DLog.ec
   easycrypt/theories/crypto/DiffieHellman.ec
   easycrypt/theories/crypto/DigitalSignatures.eca
   easycrypt/theories/crypto/DigitalSignaturesROM.eca
   easycrypt/theories/crypto/GlobalHybrid.ec
   easycrypt/theories/crypto/KeyEncapsulationMechanisms.eca
   easycrypt/theories/crypto/KeyEncapsulationMechanismsROM.eca
   easycrypt/theories/crypto/KeyedHashFunctions.eca
   easycrypt/theories/crypto/LorR.eca
   easycrypt/theories/crypto/MAC.ec
   easycrypt/theories/crypto/OW.ec
   easycrypt/theories/crypto/PKE.ec
   easycrypt/theories/crypto/PKS.ec
   easycrypt/theories/crypto/PRF.eca
   easycrypt/theories/crypto/PRG.eca
   easycrypt/theories/crypto/PROM.ec
   easycrypt/theories/crypto/PRP.eca
   easycrypt/theories/crypto/PublicKeyEncryption.eca
   easycrypt/theories/crypto/PublicKeyEncryptionROM.eca
   easycrypt/theories/crypto/ROM.eca
   easycrypt/theories/crypto/RndExcept.eca
   easycrypt/theories/crypto/SecureChannels.ec
   easycrypt/theories/crypto/SigmaProtocol.ec
   easycrypt/theories/crypto/SplitRO.ec
   easycrypt/theories/crypto/SymmetricEncryption.ec
   easycrypt/theories/crypto/TweakableHashFunctions.eca
   easycrypt/theories/crypto/assumptions/AEAD.ec
   easycrypt/theories/crypto/assumptions/CRHash.ec
   easycrypt/theories/crypto/assumptions/DHIES.ec
   easycrypt/theories/crypto/assumptions/MRPKE.ec
   easycrypt/theories/crypto/assumptions/ODH.ec
   easycrypt/theories/crypto/assumptions/PKSMK.ec
   easycrypt/theories/crypto/pke/PKE_CPA.eca
   easycrypt/theories/crypto/prp_prf/Strong_RP_RF.eca
   easycrypt/theories/crypto/ske/CCA.eca
   easycrypt/theories/crypto/ske/CCA1.eca
   easycrypt/theories/crypto/ske/CPA.eca
   easycrypt/theories/crypto/ske/NewSKE.eca
   easycrypt/theories/datatypes/Array.ec
   easycrypt/theories/datatypes/BitEncoding.ec
   easycrypt/theories/datatypes/BitWord.eca
   easycrypt/theories/datatypes/FMap.ec
   easycrypt/theories/datatypes/FSet.ec
   easycrypt/theories/datatypes/FloorCeil.ec
   easycrypt/theories/datatypes/Int.ec
   easycrypt/theories/datatypes/IntMin.ec
   easycrypt/theories/datatypes/List.ec
   easycrypt/theories/datatypes/MSet.ec
   easycrypt/theories/datatypes/QFABV.ec
   easycrypt/theories/datatypes/Real.ec
   easycrypt/theories/datatypes/SmtMap.ec
   easycrypt/theories/datatypes/Tuple.eca
   easycrypt/theories/datatypes/Word.eca
   easycrypt/theories/datatypes/Xint.ec
   easycrypt/theories/datatypes/Xreal.ec
   easycrypt/theories/distributions/DBool.ec
   easycrypt/theories/distributions/DInterval.ec
   easycrypt/theories/distributions/DJoin.ec
   easycrypt/theories/distributions/DList.ec
   easycrypt/theories/distributions/DMap.ec
   easycrypt/theories/distributions/DProd.ec
   easycrypt/theories/distributions/Dexcepted.ec
   easycrypt/theories/distributions/Dfilter.ec
   easycrypt/theories/distributions/Distr.ec
   easycrypt/theories/distributions/Mu_mem.ec
   easycrypt/theories/distributions/SDist.ec
   easycrypt/theories/encryption/DDH_hybrid.ec
   easycrypt/theories/encryption/Hybrid.ec
   easycrypt/theories/encryption/Indist.ec
   easycrypt/theories/encryption/Means.ec
   easycrypt/theories/encryption/PKE_hybrid.ec
   easycrypt/theories/encryption/SampleBool.ec
   easycrypt/theories/looping/FoldProc.eca
   easycrypt/theories/looping/IterProc.eca
   easycrypt/theories/looping/LoopTransform.ec
   easycrypt/theories/modules/EventPartitioning.ec
   easycrypt/theories/modules/ModuleStructure.ec
   easycrypt/theories/modules/PlugAndPray.eca
   easycrypt/theories/modules/Pr_half.eca
   easycrypt/theories/modules/Reflection.eca
   easycrypt/theories/modules/RndProd.eca
   easycrypt/theories/modules/TotalProb.ec
   easycrypt/theories/prelude/Logic.ec
   easycrypt/theories/prelude/Pervasive.ec
   easycrypt/theories/prelude/Tactics.ec
   easycrypt/theories/query_counting/Counter.eca
   easycrypt/theories/query_counting/OracleBounds.ec
   easycrypt/theories/structure/Discrete.ec
   easycrypt/theories/structure/FinType.ec
   easycrypt/theories/structure/Finite.ec
   easycrypt/theories/structure/Quotient.ec
   easycrypt/theories/structure/Subtype.eca
   easycrypt/theories/structure/WF.ec
   easycrypt/theories/tactics/AlgTactic.ec
   easycrypt/theories/tactics/FelTactic.ec))
 (libexec (ecLib/ecLib.cmxs inifiles/inifiles.cmxs lospecs/lospecs.cmxs))
 (libexec_root (easycrypt/commands/runtest))
 (bin (easycrypt ec-runtest))
 (doc (LICENSE README.md))
 (stublibs (dllecLib_stubs.so)))
(library
 (name easycrypt.ecLib)
 (kind normal)
 (archives (byte ecLib/ecLib.cma) (native ecLib/ecLib.cmxa))
 (plugins (byte ecLib/ecLib.cma) (native ecLib/ecLib.cmxs))
 (foreign_objects ecLib/eunix.o)
 (foreign_archives (archives (for all) (files ecLib/libecLib_stubs.a)))
 (foreign_dll_files ../stublibs/dllecLib_stubs.so)
 (native_archives ecLib/ecLib.a)
 (requires
  batteries
  camlp-streams
  dune-build-info
  dune-private-libs.dune-section
  dune-site
  easycrypt.inifiles
  easycrypt.lospecs
  markdown
  markdown.html
  pcre2
  tyxml
  why3
  yojson
  zarith)
 (main_module_name EcLib)
 (modes byte native)
 (modules
  (wrapped
   (group
    (alias
     (obj_name ecLib)
     (visibility public)
     (kind alias)
     (source (path EcLib) (impl (path ecLib/ecLib.ml-gen))))
    (name EcLib)
    (modules
     (module
      (obj_name ecLib__EUnix)
      (visibility public)
      (source
       (path EUnix)
       (intf (path ecLib/system/EUnix.mli))
       (impl (path ecLib/system/EUnix.ml))))
     (module
      (obj_name ecLib__EcAlgTactic)
      (visibility public)
      (source
       (path EcAlgTactic)
       (intf (path ecLib/ecAlgTactic.mli))
       (impl (path ecLib/ecAlgTactic.ml))))
     (module
      (obj_name ecLib__EcAlgebra)
      (visibility public)
      (source
       (path EcAlgebra)
       (intf (path ecLib/ecAlgebra.mli))
       (impl (path ecLib/ecAlgebra.ml))))
     (module
      (obj_name ecLib__EcAlphaInvHashtbl)
      (visibility public)
      (source
       (path EcAlphaInvHashtbl)
       (intf (path ecLib/ecAlphaInvHashtbl.mli))
       (impl (path ecLib/ecAlphaInvHashtbl.ml))))
     (module
      (obj_name ecLib__EcAst)
      (visibility public)
      (source
       (path EcAst)
       (intf (path ecLib/ecAst.mli))
       (impl (path ecLib/ecAst.ml))))
     (module
      (obj_name ecLib__EcBaseLogic)
      (visibility public)
      (source (path EcBaseLogic) (impl (path ecLib/ecBaseLogic.ml))))
     (module
      (obj_name ecLib__EcBigInt)
      (visibility public)
      (source
       (path EcBigInt)
       (intf (path ecLib/ecBigInt.mli))
       (impl (path ecLib/ecBigInt.ml))))
     (module
      (obj_name ecLib__EcBigIntCore)
      (visibility public)
      (source (path EcBigIntCore) (impl (path ecLib/ecBigIntCore.ml))))
     (module
      (obj_name ecLib__EcBullets)
      (visibility public)
      (source
       (path EcBullets)
       (intf (path ecLib/ecBullets.mli))
       (impl (path ecLib/ecBullets.ml))))
     (module
      (obj_name ecLib__EcCallbyValue)
      (visibility public)
      (source
       (path EcCallbyValue)
       (intf (path ecLib/ecCallbyValue.mli))
       (impl (path ecLib/ecCallbyValue.ml))))
     (module
      (obj_name ecLib__EcCircuits)
      (visibility public)
      (source
       (path EcCircuits)
       (intf (path ecLib/ecCircuits.mli))
       (impl (path ecLib/ecCircuits.ml))))
     (module
      (obj_name ecLib__EcCommands)
      (visibility public)
      (source
       (path EcCommands)
       (intf (path ecLib/ecCommands.mli))
       (impl (path ecLib/ecCommands.ml))))
     (module
      (obj_name ecLib__EcCoq)
      (visibility public)
      (source
       (path EcCoq)
       (intf (path ecLib/ecCoq.mli))
       (impl (path ecLib/ecCoq.ml))))
     (module
      (obj_name ecLib__EcCoreFol)
      (visibility public)
      (source
       (path EcCoreFol)
       (intf (path ecLib/ecCoreFol.mli))
       (impl (path ecLib/ecCoreFol.ml))))
     (module
      (obj_name ecLib__EcCoreGoal)
      (visibility public)
      (source
       (path EcCoreGoal)
       (intf (path ecLib/ecCoreGoal.mli))
       (impl (path ecLib/ecCoreGoal.ml))))
     (module
      (obj_name ecLib__EcCoreLib)
      (visibility public)
      (source
       (path EcCoreLib)
       (intf (path ecLib/ecCoreLib.mli))
       (impl (path ecLib/ecCoreLib.ml))))
     (module
      (obj_name ecLib__EcCoreModules)
      (visibility public)
      (source
       (path EcCoreModules)
       (intf (path ecLib/ecCoreModules.mli))
       (impl (path ecLib/ecCoreModules.ml))))
     (module
      (obj_name ecLib__EcCorePrinting)
      (visibility public)
      (source (path EcCorePrinting) (impl (path ecLib/ecCorePrinting.ml))))
     (module
      (obj_name ecLib__EcCoreSubst)
      (visibility public)
      (source
       (path EcCoreSubst)
       (intf (path ecLib/ecCoreSubst.mli))
       (impl (path ecLib/ecCoreSubst.ml))))
     (module
      (obj_name ecLib__EcDecl)
      (visibility public)
      (source
       (path EcDecl)
       (intf (path ecLib/ecDecl.mli))
       (impl (path ecLib/ecDecl.ml))))
     (module
      (obj_name ecLib__EcDoc)
      (visibility public)
      (source
       (path EcDoc)
       (intf (path ecLib/ecDoc.mli))
       (impl (path ecLib/ecDoc.ml))))
     (module
      (obj_name ecLib__EcDuneSites)
      (visibility public)
      (source (path EcDuneSites) (impl (path ecLib/EcDuneSites.ml))))
     (module
      (obj_name ecLib__EcEco)
      (visibility public)
      (source (path EcEco) (impl (path ecLib/ecEco.ml))))
     (module
      (obj_name ecLib__EcEnv)
      (visibility public)
      (source
       (path EcEnv)
       (intf (path ecLib/ecEnv.mli))
       (impl (path ecLib/ecEnv.ml))))
     (module
      (obj_name ecLib__EcField)
      (visibility public)
      (source
       (path EcField)
       (intf (path ecLib/ecField.mli))
       (impl (path ecLib/ecField.ml))))
     (module
      (obj_name ecLib__EcFol)
      (visibility public)
      (source
       (path EcFol)
       (intf (path ecLib/ecFol.mli))
       (impl (path ecLib/ecFol.ml))))
     (module
      (obj_name ecLib__EcGState)
      (visibility public)
      (source
       (path EcGState)
       (intf (path ecLib/ecGState.mli))
       (impl (path ecLib/ecGState.ml))))
     (module
      (obj_name ecLib__EcGenRegexp)
      (visibility public)
      (source (path EcGenRegexp) (impl (path ecLib/ecGenRegexp.ml))))
     (module
      (obj_name ecLib__EcHiGoal)
      (visibility public)
      (source
       (path EcHiGoal)
       (intf (path ecLib/ecHiGoal.mli))
       (impl (path ecLib/ecHiGoal.ml))))
     (module
      (obj_name ecLib__EcHiInductive)
      (visibility public)
      (source
       (path EcHiInductive)
       (intf (path ecLib/ecHiInductive.mli))
       (impl (path ecLib/ecHiInductive.ml))))
     (module
      (obj_name ecLib__EcHiNotations)
      (visibility public)
      (source
       (path EcHiNotations)
       (intf (path ecLib/ecHiNotations.mli))
       (impl (path ecLib/ecHiNotations.ml))))
     (module
      (obj_name ecLib__EcHiPredicates)
      (visibility public)
      (source
       (path EcHiPredicates)
       (intf (path ecLib/ecHiPredicates.mli))
       (impl (path ecLib/ecHiPredicates.ml))))
     (module
      (obj_name ecLib__EcHiTacticals)
      (visibility public)
      (source
       (path EcHiTacticals)
       (intf (path ecLib/ecHiTacticals.mli))
       (impl (path ecLib/ecHiTacticals.ml))))
     (module
      (obj_name ecLib__EcIdent)
      (visibility public)
      (source
       (path EcIdent)
       (intf (path ecLib/ecIdent.mli))
       (impl (path ecLib/ecIdent.ml))))
     (module
      (obj_name ecLib__EcInductive)
      (visibility public)
      (source
       (path EcInductive)
       (intf (path ecLib/ecInductive.mli))
       (impl (path ecLib/ecInductive.ml))))
     (module
      (obj_name ecLib__EcIo)
      (visibility public)
      (source
       (path EcIo)
       (intf (path ecLib/ecIo.mli))
       (impl (path ecLib/ecIo.ml))))
     (module
      (obj_name ecLib__EcLexer)
      (visibility public)
      (source (path EcLexer) (impl (path ecLib/ecLexer.ml))))
     (module
      (obj_name ecLib__EcLoader)
      (visibility public)
      (source
       (path EcLoader)
       (intf (path ecLib/ecLoader.mli))
       (impl (path ecLib/ecLoader.ml))))
     (module
      (obj_name ecLib__EcLocation)
      (visibility public)
      (source
       (path EcLocation)
       (intf (path ecLib/ecLocation.mli))
       (impl (path ecLib/ecLocation.ml))))
     (module
      (obj_name ecLib__EcLowCircuits)
      (visibility public)
      (source
       (path EcLowCircuits)
       (intf (path ecLib/ecLowCircuits.mli))
       (impl (path ecLib/ecLowCircuits.ml))))
     (module
      (obj_name ecLib__EcLowGoal)
      (visibility public)
      (source
       (path EcLowGoal)
       (intf (path ecLib/ecLowGoal.mli))
       (impl (path ecLib/ecLowGoal.ml))))
     (module
      (obj_name ecLib__EcLowPhlGoal)
      (visibility public)
      (source (path EcLowPhlGoal) (impl (path ecLib/ecLowPhlGoal.ml))))
     (module
      (obj_name ecLib__EcMaps)
      (visibility public)
      (source (path EcMaps) (impl (path ecLib/ecMaps.ml))))
     (module
      (obj_name ecLib__EcMatching)
      (visibility public)
      (source
       (path EcMatching)
       (intf (path ecLib/ecMatching.mli))
       (impl (path ecLib/ecMatching.ml))))
     (module
      (obj_name ecLib__EcMemory)
      (visibility public)
      (source
       (path EcMemory)
       (intf (path ecLib/ecMemory.mli))
       (impl (path ecLib/ecMemory.ml))))
     (module
      (obj_name ecLib__EcModules)
      (visibility public)
      (source
       (path EcModules)
       (intf (path ecLib/ecModules.mli))
       (impl (path ecLib/ecModules.ml))))
     (module
      (obj_name ecLib__EcOptions)
      (visibility public)
      (source
       (path EcOptions)
       (intf (path ecLib/ecOptions.mli))
       (impl (path ecLib/ecOptions.ml))))
     (module
      (obj_name ecLib__EcPException)
      (visibility public)
      (source
       (path EcPException)
       (intf (path ecLib/ecPException.mli))
       (impl (path ecLib/ecPException.ml))))
     (module
      (obj_name ecLib__EcPV)
      (visibility public)
      (source
       (path EcPV)
       (intf (path ecLib/ecPV.mli))
       (impl (path ecLib/ecPV.ml))))
     (module
      (obj_name ecLib__EcParser)
      (visibility public)
      (source
       (path EcParser)
       (intf (path ecLib/ecParser.mli))
       (impl (path ecLib/ecParser.ml))))
     (module
      (obj_name ecLib__EcParsetree)
      (visibility public)
      (source (path EcParsetree) (impl (path ecLib/ecParsetree.ml))))
     (module
      (obj_name ecLib__EcPath)
      (visibility public)
      (source
       (path EcPath)
       (intf (path ecLib/ecPath.mli))
       (impl (path ecLib/ecPath.ml))))
     (module
      (obj_name ecLib__EcPhlAuto)
      (visibility public)
      (source
       (path EcPhlAuto)
       (intf (path ecLib/phl/ecPhlAuto.mli))
       (impl (path ecLib/phl/ecPhlAuto.ml))))
     (module
      (obj_name ecLib__EcPhlBDep)
      (visibility public)
      (source
       (path EcPhlBDep)
       (intf (path ecLib/phl/ecPhlBDep.mli))
       (impl (path ecLib/phl/ecPhlBDep.ml))))
     (module
      (obj_name ecLib__EcPhlBdHoare)
      (visibility public)
      (source
       (path EcPhlBdHoare)
       (intf (path ecLib/phl/ecPhlBdHoare.mli))
       (impl (path ecLib/phl/ecPhlBdHoare.ml))))
     (module
      (obj_name ecLib__EcPhlCall)
      (visibility public)
      (source
       (path EcPhlCall)
       (intf (path ecLib/phl/ecPhlCall.mli))
       (impl (path ecLib/phl/ecPhlCall.ml))))
     (module
      (obj_name ecLib__EcPhlCase)
      (visibility public)
      (source
       (path EcPhlCase)
       (intf (path ecLib/phl/ecPhlCase.mli))
       (impl (path ecLib/phl/ecPhlCase.ml))))
     (module
      (obj_name ecLib__EcPhlCodeTx)
      (visibility public)
      (source
       (path EcPhlCodeTx)
       (intf (path ecLib/phl/ecPhlCodeTx.mli))
       (impl (path ecLib/phl/ecPhlCodeTx.ml))))
     (module
      (obj_name ecLib__EcPhlCond)
      (visibility public)
      (source
       (path EcPhlCond)
       (intf (path ecLib/phl/ecPhlCond.mli))
       (impl (path ecLib/phl/ecPhlCond.ml))))
     (module
      (obj_name ecLib__EcPhlConseq)
      (visibility public)
      (source
       (path EcPhlConseq)
       (intf (path ecLib/phl/ecPhlConseq.mli))
       (impl (path ecLib/phl/ecPhlConseq.ml))))
     (module
      (obj_name ecLib__EcPhlCoreView)
      (visibility public)
      (source
       (path EcPhlCoreView)
       (intf (path ecLib/phl/ecPhlCoreView.mli))
       (impl (path ecLib/phl/ecPhlCoreView.ml))))
     (module
      (obj_name ecLib__EcPhlDeno)
      (visibility public)
      (source
       (path EcPhlDeno)
       (intf (path ecLib/phl/ecPhlDeno.mli))
       (impl (path ecLib/phl/ecPhlDeno.ml))))
     (module
      (obj_name ecLib__EcPhlEager)
      (visibility public)
      (source
       (path EcPhlEager)
       (intf (path ecLib/phl/ecPhlEager.mli))
       (impl (path ecLib/phl/ecPhlEager.ml))))
     (module
      (obj_name ecLib__EcPhlEqobs)
      (visibility public)
      (source
       (path EcPhlEqobs)
       (intf (path ecLib/phl/ecPhlEqobs.mli))
       (impl (path ecLib/phl/ecPhlEqobs.ml))))
     (module
      (obj_name ecLib__EcPhlExists)
      (visibility public)
      (source
       (path EcPhlExists)
       (intf (path ecLib/phl/ecPhlExists.mli))
       (impl (path ecLib/phl/ecPhlExists.ml))))
     (module
      (obj_name ecLib__EcPhlFel)
      (visibility public)
      (source
       (path EcPhlFel)
       (intf (path ecLib/phl/ecPhlFel.mli))
       (impl (path ecLib/phl/ecPhlFel.ml))))
     (module
      (obj_name ecLib__EcPhlFun)
      (visibility public)
      (source
       (path EcPhlFun)
       (intf (path ecLib/phl/ecPhlFun.mli))
       (impl (path ecLib/phl/ecPhlFun.ml))))
     (module
      (obj_name ecLib__EcPhlHiAuto)
      (visibility public)
      (source
       (path EcPhlHiAuto)
       (intf (path ecLib/phl/ecPhlHiAuto.mli))
       (impl (path ecLib/phl/ecPhlHiAuto.ml))))
     (module
      (obj_name ecLib__EcPhlHiBdHoare)
      (visibility public)
      (source
       (path EcPhlHiBdHoare)
       (intf (path ecLib/phl/ecPhlHiBdHoare.mli))
       (impl (path ecLib/phl/ecPhlHiBdHoare.ml))))
     (module
      (obj_name ecLib__EcPhlHiCond)
      (visibility public)
      (source
       (path EcPhlHiCond)
       (intf (path ecLib/phl/ecPhlHiCond.mli))
       (impl (path ecLib/phl/ecPhlHiCond.ml))))
     (module
      (obj_name ecLib__EcPhlHoare)
      (visibility public)
      (source
       (path EcPhlHoare)
       (intf (path ecLib/phl/ecPhlHoare.mli))
       (impl (path ecLib/phl/ecPhlHoare.ml))))
     (module
      (obj_name ecLib__EcPhlInline)
      (visibility public)
      (source
       (path EcPhlInline)
       (intf (path ecLib/phl/ecPhlInline.mli))
       (impl (path ecLib/phl/ecPhlInline.ml))))
     (module
      (obj_name ecLib__EcPhlLoopTx)
      (visibility public)
      (source
       (path EcPhlLoopTx)
       (intf (path ecLib/phl/ecPhlLoopTx.mli))
       (impl (path ecLib/phl/ecPhlLoopTx.ml))))
     (module
      (obj_name ecLib__EcPhlOutline)
      (visibility public)
      (source
       (path EcPhlOutline)
       (intf (path ecLib/phl/ecPhlOutline.mli))
       (impl (path ecLib/phl/ecPhlOutline.ml))))
     (module
      (obj_name ecLib__EcPhlPr)
      (visibility public)
      (source
       (path EcPhlPr)
       (intf (path ecLib/phl/ecPhlPr.mli))
       (impl (path ecLib/phl/ecPhlPr.ml))))
     (module
      (obj_name ecLib__EcPhlPrRw)
      (visibility public)
      (source
       (path EcPhlPrRw)
       (intf (path ecLib/phl/ecPhlPrRw.mli))
       (impl (path ecLib/phl/ecPhlPrRw.ml))))
     (module
      (obj_name ecLib__EcPhlRCond)
      (visibility public)
      (source
       (path EcPhlRCond)
       (intf (path ecLib/phl/ecPhlRCond.mli))
       (impl (path ecLib/phl/ecPhlRCond.ml))))
     (module
      (obj_name ecLib__EcPhlRewrite)
      (visibility public)
      (source
       (path EcPhlRewrite)
       (intf (path ecLib/phl/ecPhlRewrite.mli))
       (impl (path ecLib/phl/ecPhlRewrite.ml))))
     (module
      (obj_name ecLib__EcPhlRnd)
      (visibility public)
      (source
       (path EcPhlRnd)
       (intf (path ecLib/phl/ecPhlRnd.mli))
       (impl (path ecLib/phl/ecPhlRnd.ml))))
     (module
      (obj_name ecLib__EcPhlRwEquiv)
      (visibility public)
      (source
       (path EcPhlRwEquiv)
       (intf (path ecLib/phl/ecPhlRwEquiv.mli))
       (impl (path ecLib/phl/ecPhlRwEquiv.ml))))
     (module
      (obj_name ecLib__EcPhlRwPrgm)
      (visibility public)
      (source (path EcPhlRwPrgm) (impl (path ecLib/phl/ecPhlRwPrgm.ml))))
     (module
      (obj_name ecLib__EcPhlSeq)
      (visibility public)
      (source
       (path EcPhlSeq)
       (intf (path ecLib/phl/ecPhlSeq.mli))
       (impl (path ecLib/phl/ecPhlSeq.ml))))
     (module
      (obj_name ecLib__EcPhlSkip)
      (visibility public)
      (source
       (path EcPhlSkip)
       (intf (path ecLib/phl/ecPhlSkip.mli))
       (impl (path ecLib/phl/ecPhlSkip.ml))))
     (module
      (obj_name ecLib__EcPhlSp)
      (visibility public)
      (source
       (path EcPhlSp)
       (intf (path ecLib/phl/ecPhlSp.mli))
       (impl (path ecLib/phl/ecPhlSp.ml))))
     (module
      (obj_name ecLib__EcPhlSwap)
      (visibility public)
      (source
       (path EcPhlSwap)
       (intf (path ecLib/phl/ecPhlSwap.mli))
       (impl (path ecLib/phl/ecPhlSwap.ml))))
     (module
      (obj_name ecLib__EcPhlSym)
      (visibility public)
      (source
       (path EcPhlSym)
       (intf (path ecLib/phl/ecPhlSym.mli))
       (impl (path ecLib/phl/ecPhlSym.ml))))
     (module
      (obj_name ecLib__EcPhlTAuto)
      (visibility public)
      (source
       (path EcPhlTAuto)
       (intf (path ecLib/phl/ecPhlTAuto.mli))
       (impl (path ecLib/phl/ecPhlTAuto.ml))))
     (module
      (obj_name ecLib__EcPhlTrans)
      (visibility public)
      (source
       (path EcPhlTrans)
       (intf (path ecLib/phl/ecPhlTrans.mli))
       (impl (path ecLib/phl/ecPhlTrans.ml))))
     (module
      (obj_name ecLib__EcPhlUpto)
      (visibility public)
      (source
       (path EcPhlUpto)
       (intf (path ecLib/phl/ecPhlUpto.mli))
       (impl (path ecLib/phl/ecPhlUpto.ml))))
     (module
      (obj_name ecLib__EcPhlWhile)
      (visibility public)
      (source
       (path EcPhlWhile)
       (intf (path ecLib/phl/ecPhlWhile.mli))
       (impl (path ecLib/phl/ecPhlWhile.ml))))
     (module
      (obj_name ecLib__EcPhlWp)
      (visibility public)
      (source
       (path EcPhlWp)
       (intf (path ecLib/phl/ecPhlWp.mli))
       (impl (path ecLib/phl/ecPhlWp.ml))))
     (module
      (obj_name ecLib__EcPrinting)
      (visibility public)
      (source
       (path EcPrinting)
       (intf (path ecLib/ecPrinting.mli))
       (impl (path ecLib/ecPrinting.ml))))
     (module
      (obj_name ecLib__EcProcSem)
      (visibility public)
      (source
       (path EcProcSem)
       (intf (path ecLib/ecProcSem.mli))
       (impl (path ecLib/ecProcSem.ml))))
     (module
      (obj_name ecLib__EcProofTerm)
      (visibility public)
      (source
       (path EcProofTerm)
       (intf (path ecLib/ecProofTerm.mli))
       (impl (path ecLib/ecProofTerm.ml))))
     (module
      (obj_name ecLib__EcProofTyping)
      (visibility public)
      (source
       (path EcProofTyping)
       (intf (path ecLib/ecProofTyping.mli))
       (impl (path ecLib/ecProofTyping.ml))))
     (module
      (obj_name ecLib__EcProvers)
      (visibility public)
      (source
       (path EcProvers)
       (intf (path ecLib/ecProvers.mli))
       (impl (path ecLib/ecProvers.ml))))
     (module
      (obj_name ecLib__EcReduction)
      (visibility public)
      (source
       (path EcReduction)
       (intf (path ecLib/ecReduction.mli))
       (impl (path ecLib/ecReduction.ml))))
     (module
      (obj_name ecLib__EcRegexp)
      (visibility public)
      (source
       (path EcRegexp)
       (intf (path ecLib/ecRegexp.mli))
       (impl (path ecLib/ecRegexp.ml))))
     (module
      (obj_name ecLib__EcRelocate)
      (visibility public)
      (source
       (path EcRelocate)
       (intf (path ecLib/ecRelocate.mli))
       (impl (path ecLib/ecRelocate.ml))))
     (module
      (obj_name ecLib__EcRing)
      (visibility public)
      (source
       (path EcRing)
       (intf (path ecLib/ecRing.mli))
       (impl (path ecLib/ecRing.ml))))
     (module
      (obj_name ecLib__EcScope)
      (visibility public)
      (source
       (path EcScope)
       (intf (path ecLib/ecScope.mli))
       (impl (path ecLib/ecScope.ml))))
     (module
      (obj_name ecLib__EcSearch)
      (visibility public)
      (source
       (path EcSearch)
       (intf (path ecLib/ecSearch.mli))
       (impl (path ecLib/ecSearch.ml))))
     (module
      (obj_name ecLib__EcSection)
      (visibility public)
      (source
       (path EcSection)
       (intf (path ecLib/ecSection.mli))
       (impl (path ecLib/ecSection.ml))))
     (module
      (obj_name ecLib__EcSimplifyContext)
      (visibility public)
      (source
       (path EcSimplifyContext)
       (intf (path ecLib/ecSimplifyContext.mli))
       (impl (path ecLib/ecSimplifyContext.ml))))
     (module
      (obj_name ecLib__EcSmt)
      (visibility public)
      (source
       (path EcSmt)
       (intf (path ecLib/ecSmt.mli))
       (impl (path ecLib/ecSmt.ml))))
     (module
      (obj_name ecLib__EcStrongRing)
      (visibility public)
      (source (path EcStrongRing) (impl (path ecLib/ecStrongRing.ml))))
     (module
      (obj_name ecLib__EcSubst)
      (visibility public)
      (source
       (path EcSubst)
       (intf (path ecLib/ecSubst.mli))
       (impl (path ecLib/ecSubst.ml))))
     (module
      (obj_name ecLib__EcSymbols)
      (visibility public)
      (source
       (path EcSymbols)
       (intf (path ecLib/ecSymbols.mli))
       (impl (path ecLib/ecSymbols.ml))))
     (module
      (obj_name ecLib__EcTerminal)
      (visibility public)
      (source
       (path EcTerminal)
       (intf (path ecLib/ecTerminal.mli))
       (impl (path ecLib/ecTerminal.ml))))
     (module
      (obj_name ecLib__EcThCloning)
      (visibility public)
      (source
       (path EcThCloning)
       (intf (path ecLib/ecThCloning.mli))
       (impl (path ecLib/ecThCloning.ml))))
     (module
      (obj_name ecLib__EcTheory)
      (visibility public)
      (source
       (path EcTheory)
       (intf (path ecLib/ecTheory.mli))
       (impl (path ecLib/ecTheory.ml))))
     (module
      (obj_name ecLib__EcTheoryReplay)
      (visibility public)
      (source
       (path EcTheoryReplay)
       (intf (path ecLib/ecTheoryReplay.mli))
       (impl (path ecLib/ecTheoryReplay.ml))))
     (module
      (obj_name ecLib__EcTransMatching)
      (visibility public)
      (source
       (path EcTransMatching)
       (intf (path ecLib/ecTransMatching.mli))
       (impl (path ecLib/ecTransMatching.ml))))
     (module
      (obj_name ecLib__EcTypeClass)
      (visibility public)
      (source
       (path EcTypeClass)
       (intf (path ecLib/ecTypeClass.mli))
       (impl (path ecLib/ecTypeClass.ml))))
     (module
      (obj_name ecLib__EcTypes)
      (visibility public)
      (source
       (path EcTypes)
       (intf (path ecLib/ecTypes.mli))
       (impl (path ecLib/ecTypes.ml))))
     (module
      (obj_name ecLib__EcTypesafeFol)
      (visibility public)
      (source
       (path EcTypesafeFol)
       (intf (path ecLib/ecTypesafeFol.mli))
       (impl (path ecLib/ecTypesafeFol.ml))))
     (module
      (obj_name ecLib__EcTyping)
      (visibility public)
      (source
       (path EcTyping)
       (intf (path ecLib/ecTyping.mli))
       (impl (path ecLib/ecTyping.ml))))
     (module
      (obj_name ecLib__EcUFind)
      (visibility public)
      (source
       (path EcUFind)
       (intf (path ecLib/ecUFind.mli))
       (impl (path ecLib/ecUFind.ml))))
     (module
      (obj_name ecLib__EcUid)
      (visibility public)
      (source
       (path EcUid)
       (intf (path ecLib/ecUid.mli))
       (impl (path ecLib/ecUid.ml))))
     (module
      (obj_name ecLib__EcUnify)
      (visibility public)
      (source
       (path EcUnify)
       (intf (path ecLib/ecUnify.mli))
       (impl (path ecLib/ecUnify.ml))))
     (module
      (obj_name ecLib__EcUnifyProc)
      (visibility public)
      (source
       (path EcUnifyProc)
       (intf (path ecLib/ecUnifyProc.mli))
       (impl (path ecLib/ecUnifyProc.ml))))
     (module
      (obj_name ecLib__EcUserMessages)
      (visibility public)
      (source
       (path EcUserMessages)
       (intf (path ecLib/ecUserMessages.mli))
       (impl (path ecLib/ecUserMessages.ml))))
     (module
      (obj_name ecLib__EcUtils)
      (visibility public)
      (source
       (path EcUtils)
       (intf (path ecLib/ecUtils.mli))
       (impl (path ecLib/ecUtils.ml))))
     (module
      (obj_name ecLib__EcVersion)
      (visibility public)
      (source
       (path EcVersion)
       (intf (path ecLib/ecVersion.mli))
       (impl (path ecLib/ecVersion.ml))))
     (module
      (obj_name ecLib__EcWhy3Conv)
      (visibility public)
      (source
       (path EcWhy3Conv)
       (intf (path ecLib/ecWhy3Conv.mli))
       (impl (path ecLib/ecWhy3Conv.ml))))
     (module
      (obj_name ecLib__XDG)
      (visibility public)
      (source
       (path XDG)
       (intf (path ecLib/system/XDG.mli))
       (impl (path ecLib/system/XDG.ml))))))
   (wrapped true))))
(library
 (name easycrypt.inifiles)
 (kind normal)
 (archives (byte inifiles/inifiles.cma) (native inifiles/inifiles.cmxa))
 (plugins (byte inifiles/inifiles.cma) (native inifiles/inifiles.cmxs))
 (native_archives inifiles/inifiles.a)
 (requires pcre2 unix)
 (main_module_name Inifiles)
 (modes byte native)
 (modules
  (wrapped
   (group
    (alias
     (obj_name inifiles__)
     (visibility public)
     (kind alias)
     (source (path Inifiles__) (impl (path inifiles/inifiles__.ml-gen))))
    (name Inifiles)
    (modules
     (module
      (obj_name inifiles)
      (visibility public)
      (source
       (path Inifiles)
       (intf (path inifiles/inifiles.mli))
       (impl (path inifiles/inifiles.ml))))
     (module
      (obj_name inifiles__Inilexer)
      (visibility public)
      (source (path Inilexer) (impl (path inifiles/inilexer.ml))))
     (module
      (obj_name inifiles__Parseini)
      (visibility public)
      (source
       (path Parseini)
       (intf (path inifiles/parseini.mli))
       (impl (path inifiles/parseini.ml))))))
   (wrapped true))))
(library
 (name easycrypt.lospecs)
 (kind normal)
 (archives (byte lospecs/lospecs.cma) (native lospecs/lospecs.cmxa))
 (plugins (byte lospecs/lospecs.cma) (native lospecs/lospecs.cmxs))
 (native_archives lospecs/lospecs.a)
 (requires batteries bitwuzla-cxx menhirLib zarith)
 (main_module_name Lospecs)
 (modes byte native)
 (modules
  (wrapped
   (group
    (alias
     (obj_name lospecs)
     (visibility public)
     (kind alias)
     (source (path Lospecs) (impl (path lospecs/lospecs.ml-gen))))
    (name Lospecs)
    (modules
     (module
      (obj_name lospecs__Aig)
      (visibility public)
      (source
       (path Aig)
       (intf (path lospecs/aig.mli))
       (impl (path lospecs/aig.ml))))
     (module
      (obj_name lospecs__Ast)
      (visibility public)
      (source
       (path Ast)
       (intf (path lospecs/ast.mli))
       (impl (path lospecs/ast.ml))))
     (module
      (obj_name lospecs__Circuit)
      (visibility public)
      (source
       (path Circuit)
       (intf (path lospecs/circuit.mli))
       (impl (path lospecs/circuit.ml))))
     (module
      (obj_name lospecs__Deps)
      (visibility public)
      (source
       (path Deps)
       (intf (path lospecs/deps.mli))
       (impl (path lospecs/deps.ml))))
     (module
      (obj_name lospecs__Io)
      (visibility public)
      (source
       (path Io)
       (intf (path lospecs/io.mli))
       (impl (path lospecs/io.ml))))
     (module
      (obj_name lospecs__Lexer)
      (visibility public)
      (source (path Lexer) (impl (path lospecs/lexer.ml))))
     (module
      (obj_name lospecs__Parser)
      (visibility public)
      (source
       (path Parser)
       (intf (path lospecs/parser.mli))
       (impl (path lospecs/parser.ml))))
     (module
      (obj_name lospecs__Ptree)
      (visibility public)
      (source
       (path Ptree)
       (intf (path lospecs/ptree.mli))
       (impl (path lospecs/ptree.ml))))
     (module
      (obj_name lospecs__Smt)
      (visibility public)
      (source
       (path Smt)
       (intf (path lospecs/smt.mli))
       (impl (path lospecs/smt.ml))))
     (module
      (obj_name lospecs__Specifications)
      (visibility public)
      (source
       (path Specifications)
       (intf (path lospecs/specifications.mli))
       (impl (path lospecs/specifications.ml))))
     (module
      (obj_name lospecs__Typing)
      (visibility public)
      (source
       (path Typing)
       (intf (path lospecs/typing.mli))
       (impl (path lospecs/typing.ml))))))
   (wrapped true))))
