_CoqProject

-arg -w -arg -notation-overridden
-arg -w -arg -non-reversible-notation

-R ../execution/theories ConCert.Execution
-R ../utils/theories ConCert.Utils

-Q theories ConCert.Embedding
theories/Ast.v
theories/CertifyingTranslate.v
theories/EnvSubst.v
theories/EvalE.v
theories/Misc.v
theories/Notations.v
theories/Prelude.v
theories/SimpleBlockchain.v
theories/Tests.v
theories/TranslationUtils.v
theories/Utils.v
theories/Wf.v
theories/pcuic/PCUICCorrectness.v
theories/pcuic/PCUICCorrectnessAux.v
theories/pcuic/PCUICFacts.v
theories/pcuic/PCUICTranslate.v
theories/pcuic/PCUICtoTemplate.v

-Q extraction ConCert.Embedding.Extraction
extraction/Liquidity.v
extraction/PreludeExt.v
extraction/SimpleBlockchainExt.v

-Q examples ConCert.Embedding.Examples
examples/AcornExamples.v
examples/Demo.v
examples/FinMap.v