emarzion · emarzion · Apr 2, 2024 · Mar 25, 2024 · Apr 2, 2024 · Apr 2, 2024
diff --git a/bin/gen/ExtractRomanWheel.v b/bin/gen/ExtractRomanWheel.v
@@ -15,4 +15,6 @@ Require Import TBGen.Bear.BearGame.
 Require Import TBGen.Bear.RomanWheel.
 Require Import TBGen.TB.TB.
 
+Set Warnings "-extraction-default-directory".
+
 Extraction "TBGen.ml" RW_TB.
diff --git a/theory/TB/SampleGame.v → theory/Sample/SampleGame.v b/theory/TB/SampleGame.v → theory/Sample/SampleGame.v
diff --git a/theory/Util/Dist.v b/theory/Util/Dist.v
diff --git a/theory/Util/Fin.v b/theory/Util/Fin.v
diff --git a/theory/Util/Mat.v b/theory/Util/Mat.v
diff --git a/theory/Util/NewLoop.v b/theory/Util/NewLoop.v
diff --git a/theory/Util/Rel.v b/theory/Util/Rel.v
diff --git a/theory/Util/SBetween.v b/theory/Util/SBetween.v
diff --git a/theory/Util/Vec.v b/theory/Util/Vec.v