_CoqProject

#-Q ./coq-library-undecidability/PCP "PCP"
-Q ./coq-library-undecidability "Undecidability"
-Q ./base-library "Shared"
-Q "./template-coq/template-coq/theories/" Template
-I "./template-coq/template-coq/src"

-R . "L"

-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files,-cannot-define-projection,-records,-unused-intro-pattern,-tactics,-masking-absolute-name

-install none
COQDOCFLAGS = "--charset utf-8 -s --parse-comments --with-header ./docs/website/resources/header.html --with-footer ./docs/website/resources/footer.html --index indexpage"

Prelim/MoreBase.v
Prelim/ARS.v
Prelim/StringBase.v
Prelim/MoreList.v

L.v

Tactics/Computable.v
Tactics/ComputableTime.v

Tactics/LTactics.v

Tactics/Extract.v
Tactics/GenEncode.v

Tactics/Lproc.v
Tactics/Lbeta.v
Tactics/Reflection.v
Tactics/LClos.v
Tactics/LClos_Eval.v
Tactics/Lrewrite.v
Tactics/Lsimpl.v

Tactics/ComputableTactics.v
Tactics/ComputableDemo.v

Tactics/mixedTactics.v

Datatypes/LUnit.v
Datatypes/LBool.v
Datatypes/LNat.v
Datatypes/Lists.v
Datatypes/LOptions.v
Datatypes/LProd.v
Datatypes/LTerm.v


Functions/Equality.v
Functions/Ackermann.v
Computability/Seval.v

Functions/Universal.v

Computability/Synthetic.v
Reductions/H10.v

TM/Prelim.v
TM/TM.v
TM/TMEncoding.v
Reductions/TM.v

Reductions/SRH_SR.v
Reductions/SR_MPCP.v
Reductions/MPCP_PCP.v
Reductions/PCP_CFG.v

Computability/Computability.v
Computability/MuRec.v