_CoqProject

-Q theories bedrock

# disable some warnings
-arg -w -arg -convert_concl_no_check
-arg -w -arg -ambiguous-paths

# Utility modules
theories/bytestring.v
theories/avl.v
theories/Util.v
theories/ChargeCompat.v
theories/ChargeUtil.v
theories/IrisBridge.v

# Syntax
theories/lang/cpp/syntax/names.v
theories/lang/cpp/syntax/types.v
theories/lang/cpp/syntax/expr.v
theories/lang/cpp/syntax/stmt.v
theories/lang/cpp/syntax/translation_unit.v
theories/lang/cpp/syntax/typing.v
theories/lang/cpp/ast.v

# Semantics
theories/lang/cpp/semantics/values.v
theories/lang/cpp/semantics/operator.v
theories/lang/cpp/semantics/sub_module.v
theories/lang/cpp/semantics.v

# Program Logic
theories/lang/cpp/logic/spec.v
theories/lang/cpp/logic/pred.v
theories/lang/cpp/logic/path_pred.v
theories/lang/cpp/logic/heap_pred.v
theories/lang/cpp/logic/intensional.v
theories/lang/cpp/logic/wp.v
theories/lang/cpp/logic/destroy.v
theories/lang/cpp/logic/destructors.v
theories/lang/cpp/logic/initializers.v
theories/lang/cpp/logic/call.v
theories/lang/cpp/logic/expr.v
theories/lang/cpp/logic/stmt.v
theories/lang/cpp/logic/func.v
theories/lang/cpp/logic/translation_unit.v
theories/lang/cpp/logic/cclogic.v
# ^^ This is probably going to be eliminated
theories/lang/cpp/logic/atomics.v
theories/lang/cpp/logic/layout.v
theories/lang/cpp/logic.v

# Notations
theories/lang/cpp/heap_notations.v
theories/lang/cpp/spec_notations.v
theories/lang/cpp/primitives.v

# Notations for cpp2v
theories/lang/cpp/parser.v

theories/lang/cpp/compile.v

theories/lang/cpp.v

# "soundness" proof
theories/lang/cpp/logic/simple_pred.v