-Q "../external/smpl/theories/" smpl
-I "../external/smpl/src/"
-Q "../external/uds-psl-base" PslBase

-Q . Undecidability

-install none
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files,cannot-define-projection,records,unused-intro-pattern,tactics
COQDOCFLAGS = "--charset utf-8 --parse-comments -s --with-header ./website/resources/header.html --with-footer ./website/resources/footer.html --index indexpage"

Shared/Prelim.v

Shared/Libs/DLW/Utils/focus.v
Shared/Libs/DLW/Utils/utils_tac.v
Shared/Libs/DLW/Utils/list_focus.v
Shared/Libs/DLW/Utils/utils_list.v
Shared/Libs/DLW/Utils/utils_nat.v
Shared/Libs/DLW/Utils/utils_string.v
Shared/Libs/DLW/Utils/utils.v
Shared/Libs/DLW/Utils/sorting.v
Shared/Libs/DLW/Utils/utils_decidable.v
Shared/Libs/DLW/Utils/interval.v

Shared/Libs/DLW/Utils/sums.v
Shared/Libs/DLW/Utils/binomial.v
Shared/Libs/DLW/Utils/bool_list.v
Shared/Libs/DLW/Utils/bool_nat.v
Shared/Libs/DLW/Utils/gcd.v
Shared/Libs/DLW/Utils/prime.v
Shared/Libs/DLW/Utils/power_decomp.v
Shared/Libs/DLW/Utils/bounded_quantification.v
Shared/Libs/DLW/Utils/php.v
Shared/Libs/DLW/Utils/rel_iter.v

Shared/Libs/DLW/Vec/pos.v
Shared/Libs/DLW/Vec/vec.v

Problems/Reduction.v
Problems/PCP.v

FOL/DecidableEnumerable.v
FOL/Reductions.v
FOL/MarkovPost.v
FOL/PCP.v
FOL/FOL.v
FOL/Semantics.v
FOL/Deduction.v
FOL/Kripke.v
FOL/BPCP_FOL.v
FOL/BPCP_IFOL.v
FOL/BPCP_CND.v
FOL/Weakening.v
FOL/Infinite.v

PCP/Definitions.v
PCP/SRH_SR.v
PCP/SR_MPCP.v
PCP/MPCP_PCP.v
PCP/PCP_CFP.v
PCP/PCP_CFI.v
PCP/singleTM.v
PCP/TM_SRH.v
PCP/Post_CFG.v
PCP/CFP_CFI.v

ILL/Definitions.v
ILL/PCP_BPCP.v
ILL/BPCP_iBPCP.v

ILL/Code/subcode.v
ILL/Code/sss.v
ILL/Code/compiler.v
#ILL/Code/compiler_new.v

ILL/Bsm/list_bool.v
ILL/Bsm/tiles_solvable.v
ILL/Bsm/bsm_defs.v
ILL/Bsm/bsm_utils.v
ILL/Bsm/bsm_pcp.v

ILL/Code/compiler_correction.v

ILL/iBPCP_BSM.v

ILL/Mm/mm_defs.v
ILL/Mm/mm_utils.v
ILL/Mm/mm_comp.v
#ILL/Mm/mm_no_self.v
#ILL/Mm/mm_comp_old.v

ILL/BSM_MM.v

ILL/Ll/ill.v
ILL/Ll/eill.v
ILL/Ll/eill_mm.v

ILL/EILL_ILL.v
ILL/MM_EILL.v

ILL/UNDEC.v

MM/mma_defs.v
MM/mma_utils.v
MM/fractran_mma.v
MM/env.v
MM/mm_instr.v
MM/mm_env_utils.v

MuRec/recalg.v
MuRec/ra_utils.v
MuRec/ra_enum.v
MuRec/ra_dio_poly.v
MuRec/ra_mm_env.v
MuRec/ra_mm.v
MuRec/ra_comp.v

H10/Fractran/mm_no_self.v
H10/Fractran/prime_seq.v
H10/Fractran/fractran_defs.v
H10/Fractran/mm_fractran.v

H10/ArithLibs/Zp.v
H10/ArithLibs/matrix.v
H10/ArithLibs/luca.v
H10/ArithLibs/lagrange.v

H10/Matija/alpha.v
H10/Matija/expo_diophantine.v
H10/Matija/cipher.v


H10/Dio/dio_logic.v
H10/Dio/dio_elem.v
H10/Dio/dio_single.v
H10/Dio/dio_expo.v
H10/Dio/dio_binary.v
H10/Dio/dio_cipher.v
H10/Dio/dio_bounded.v
H10/Dio/dio_rt_closure.v

H10/Fractran/fractran_dio.v

H10/HALT_MM.v
H10/MM_FRACTRAN.v
H10/FRACTRAN_DIO.v
H10/H10.v
H10/DPRM.v


# Basics
TM/Prelim.v
TM/Relations.v
TM/TM.v
TM/ArithPrelim.v

# Basic Machines
TM/Basic/Basic.v
TM/Basic/Null.v
TM/Basic/Mono.v
TM/Basic/Duo.v

# Programming combinators
TM/Combinators/Combinators.v
TM/Combinators/Switch.v
TM/Combinators/SequentialComposition.v
TM/Combinators/If.v
TM/Combinators/While.v
TM/Combinators/StateWhile.v
TM/Combinators/Mirror.v

# Machine Lifting
TM/Lifting/Lifting.v
TM/Lifting/LiftTapes.v
TM/Lifting/LiftAlphabet.v

# Compound Machines
TM/Compound/TMTac.v
TM/Compound/Multi.v
TM/Compound/WriteString.v
TM/Compound/MoveToSymbol.v
TM/Compound/CopySymbols.v
TM/Compound/Shift.v
TM/Compound/Compare.v

# Programming
TM/Code/Code.v
TM/Code/CodeTM.v
TM/Code/WriteValue.v
TM/Code/ChangeAlphabet.v
TM/Code/Copy.v
TM/Code/CompareValue.v
TM/Code/ProgrammingTools.v

# Cases and constructors
TM/Code/CaseNat.v
TM/Code/CaseSum.v
TM/Code/CaseList.v
TM/Code/CaseFin.v
TM/Code/CasePair.v

# Programming case studies
#TM/Code/SumTM.v
TM/Code/NatTM.v
TM/Code/ListTM.v

# Binary Numbers
TM/Code/BinNumbers/EncodeBinNumbers.v
TM/Code/BinNumbers/PosDefinitions.v
TM/Code/BinNumbers/PosPointers.v
TM/Code/BinNumbers/PosHelperMachines.v
TM/Code/BinNumbers/PosIncrementTM.v
TM/Code/BinNumbers/PosCompareTM.v
TM/Code/BinNumbers/PosShiftTM.v
TM/Code/BinNumbers/PosAddTM.v
TM/Code/BinNumbers/PosMultTM.v
TM/Code/BinNumbers/NTM.v

# Multi-Tape to Single-Tape Compiler
TM/Single/EncodeTapes.v
TM/Single/StepTM.v

# Univ
TM/Univ/LookupAssociativeListTM.v
TM/Univ/StepTM.v

# PrettyBounds
TM/PrettyBounds/PrettyBounds.v
TM/PrettyBounds/MaxList.v
TM/PrettyBounds/BaseCode.v
TM/PrettyBounds/UnivBounds.v
TM/PrettyBounds/M2MBounds.v

TM/PrettyBounds/SpaceBounds.v
TM/PrettyBounds/BaseCodeSpace.v
TM/PrettyBounds/UnivSpaceBounds.v

# Multi-Univ Simulation Theorem
TM/MultiUnivTimeSpaceSimulation.v

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

L/L.v

L/Tactics/Computable.v
L/Tactics/ComputableTime.v

L/Tactics/LTactics.v

L/Tactics/Extract.v
L/Tactics/GenEncode.v

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

L/Tactics/ComputableTactics.v
L/Tactics/ComputableDemo.v

L/Tactics/mixedTactics.v

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

L/Functions/Equality.v
L/Functions/Encoding.v
L/Functions/Proc.v
L/Functions/Size.v
L/Functions/Subst.v
L/Functions/Eval.v
L/Functions/IterupN.v

L/Functions/EnumInt.v
L/Functions/Unenc.v
L/Functions/Ackermann.v

L/TM/TMEncoding.v
L/Reductions/TM_to_L.v

L/Reductions/SRH_SR_computable.v
L/Reductions/SR_MPCP_computable.v
L/Reductions/MPCP_PCP_computable.v
L/Reductions/PCP_CFG_computable.v
L/Reductions/H10_to_L.v

L/Complexity/ResourceMeasures.v
L/Complexity/SpaceBoundsTime.v

L/AbstractMachines/Programs.v
L/AbstractMachines/AbstractSubstMachine.v
L/AbstractMachines/AbstractHeapMachine.v
L/AbstractMachines/UnfoldHeap.v
L/AbstractMachines/FunctionalDefinitions.v
L/AbstractMachines/Computable/Shared.v
L/AbstractMachines/Computable/HeapMachine.v
L/AbstractMachines/Computable/SubstMachine.v

L/Computability/Acceptability.v
#L/Computability/AD.v
L/Computability/Computability.v
#L/Computability/DA.v
L/Computability/Decidability.v
L/Computability/Enum.v
L/Computability/Fixpoints.v
#L/Computability/MoreAcc.v
L/Computability/MuRec.v
L/Computability/Partial.v
L/Computability/Por.v
#L/Computability/RE.v
L/Computability/Rice.v
L/Computability/Scott.v
L/Computability/Seval.v
L/Computability/Synthetic.v

#Reduction L to TM with abstract Heap Machine
LAM/BaseExtension.v
LAM/Prelims.v
LAM/LM_heap_def.v
LAM/LM_heap_correct.v
# Abstract Machine simulator
LAM/TM/SizeAnalysis.v
LAM/TM/Alphabets.v
LAM/TM/CaseCom.v
LAM/TM/LookupTM.v
LAM/TM/JumpTargetTM.v
LAM/TM/StepTM.v
LAM/TM/HaltingProblem.v
LAM/TM/LMBounds.v

## Higher order unficiation

HOU/std/tactics.v
HOU/std/misc.v
HOU/std/decidable.v
HOU/std/lists/basics.v
HOU/std/lists/misc.v
HOU/std/lists/advanced.v
HOU/std/countability.v
HOU/std/retracts.v
HOU/std/enumerable.v
HOU/std/reductions.v
HOU/std/ars/basic.v
HOU/std/ars/confluence.v
HOU/std/ars/normalisation.v
HOU/std/ars/evaluator.v
HOU/std/ars/list_reduction.v
HOU/std/std.v

HOU/axioms.v
HOU/unscoped.v

HOU/calculus/terms.v
HOU/calculus/prelim.v
HOU/calculus/syntax.v
HOU/calculus/semantics.v
HOU/calculus/equivalence.v
HOU/calculus/typing.v
HOU/calculus/order.v
HOU/calculus/terms_extension.v
HOU/calculus/confluence.v
HOU/calculus/normalisation.v
HOU/calculus/evaluator.v
HOU/calculus/calculus.v

HOU/unification/higher_order_unification.v
HOU/unification/systemunification.v
HOU/unification/nth_order_unification.v
HOU/unification/enumerability.v
HOU/unification/unification.v

HOU/third_order/pcp.v
HOU/third_order/encoding.v
HOU/third_order/simplified.v
HOU/third_order/huet.v

HOU/second_order/diophantine_equations.v
HOU/second_order/dowek/encoding.v
HOU/second_order/dowek/reduction.v
HOU/second_order/goldfarb/encoding.v
HOU/second_order/goldfarb/multiplication.v
HOU/second_order/goldfarb/reduction.v
HOU/second_order/goldfarb/motivation.v

HOU/concon/conservativity.v
HOU/concon/constants.v
HOU/concon/enumerability.v
HOU/concon/concon.v

HOU/firstorder.v


FOLP/axioms.v
FOLP/unscoped.v
FOLP/Syntax.v
FOLP/FOL.v
FOLP/FullSyntax.v
FOLP/FullFOL.v
FOLP/FullTarski.v
FOLP/Input.v

Problems/FOL.v
Problems/TM.v
Problems/SR.v
Problems/MM.v
Problems/MM2.v
Problems/BSM.v
Problems/ILL.v
Problems/FRACTRAN.v
Problems/DIOPHANTINE.v
Problems/H10C.v
Problems/cbvLambda.v
Problems/FOLFS.v

Reductions/TM_to_SRH.v  
Reductions/SRH_to_SR.v  
Reductions/SR_to_MPCP.v 
Reductions/MPCP_to_PCP.v
Reductions/PCP_to_BPCP.v
Reductions/BPCP_to_BSM.v
Reductions/BSM_to_MM.v  
Reductions/MM_to_ILL.v  
Reductions/BPCP_to_FOL.v
Reductions/DIO_MUREC.v
Reductions/MUREC_MM.v
Reductions/MMA2_to_MM2.v
Reductions/MM_to_MMA2.v
Reductions/MM_to_FRACTRAN.v
Reductions/FRACTRAN_to_H10C.v
Reductions/L_to_mTM.v
Reductions/mTM_to_TM.v
Reductions/BPCP_to_FOLFS.v