_CoqProject

# Suppress harmless compiler warnings we can't do anything about.
-arg -w -arg -projection-no-head-constant
-arg -w -arg -notation-overridden
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -notation-incompatible-format

-Q theories CompDecModal

# Shared Libs
theories/libs/bcase.v
theories/libs/edone.v
theories/libs/base.v
theories/libs/fset.v
theories/libs/fset_tac.v
theories/libs/induced_sym.v
theories/libs/modular_hilbert.v
theories/libs/sltype.v
theories/libs/rewrite_inequality.v

# K
theories/K/K_def.v
theories/K/demo.v
theories/K/hilbert_ref.v
theories/K/gentzen.v
theories/K/universal_model.v
theories/K/results.v

# Kstar
theories/Kstar/Kstar_def.v
theories/Kstar/demo.v
theories/Kstar/hilbert_ref.v
theories/Kstar/gen_def.v
theories/Kstar/gen_ref.v
theories/Kstar/results.v

# CTL
theories/CTL/CTL_def.v
theories/CTL/hilbert.v
theories/CTL/dags.v
theories/CTL/demo.v
theories/CTL/relaxed_pruning.v
theories/CTL/hilbert_ref.v
theories/CTL/hilbert_Eme90.v
theories/CTL/hilbert_LS.v
theories/CTL/agreement.v
theories/CTL/gen_def.v
theories/CTL/hilbert_hist.v
theories/CTL/gen_hsound.v
theories/CTL/gen_ref.v
theories/CTL/gen_dec.v
theories/CTL/results.v

# PDL
theories/PDL/PDL_def.v
theories/PDL/demo.v
theories/PDL/hilbert_ref.v

# CPDL
theories/CPDL/PDL_def.v
theories/CPDL/demo.v
theories/CPDL/hilbert_ref.v