-install none
-Q . Pactole
-arg -w
-arg -notation-overridden
# Spaces in args are not supported, see Makefile.local
#-arg -set
#-arg "Suggest Proof Using=true"

## External libraries
#Util/FSets/OrderedType.v
Util/FSets/FSetInterface.v
Util/FSets/FSetFacts.v
Util/FSets/FSetList.v
Util/FMaps/FMapInterface.v
Util/FMaps/FMapFacts.v
Util/FMaps/FMapList.v
Util/MMultiset/MMultisetInterface.v
Util/MMultiset/MMultisetWMap.v
Util/MMultiset/MMultisetFacts.v
Util/MMultiset/MMultisetExtraOps.v
Util/MMultiset/Preliminary.v

## Core
Util/Preliminary.v
Util/SetoidDefs.v
Util/NumberComplements.v
Util/ListComplements.v
Util/Coqlib.v
Util/Bijection.v
Util/Stream.v
Util/Lexprod.v
Util/Ratio.v
Core/Identifiers.v
Core/State.v
Core/Configuration.v
Core/Formalism.v
Setting.v

## Models
Models/Flexible.v
Models/Rigid.v
Models/RigidFlexibleEquivalence.v
Models/RigidFlexibleEquivalence_Assumptions.v
Models/DiscreteGraph.v
Models/Similarity.v
Models/ContinuousGraph.v
Models/GraphEquivalence.v

## Spaces
Spaces/RealVectorSpace.v
Spaces/RealMetricSpace.v
Spaces/RealNormedSpace.v
Spaces/EuclideanSpace.v
Spaces/Similarity.v
Spaces/R.v
Spaces/R2.v
Spaces/Graph.v
Spaces/Isomorphism.v
Spaces/Ring.v
Spaces/Grid.v

## Observations
Observations/Definition.v
Observations/MultisetObservation.v
Observations/SetObservation.v
Observations/LimitedSetObservation.v
Observations/LimitedMultisetObservation.v
Observations/PointedObservation.v
Observations/PreCompositionObservation.v


## Case Study: Volume
CaseStudies/Volumes/NoCollisionAndPath.v