Move duper.maxSaturationTime option out of Duper namespace

leanprover-community · Feb 14, 2025 · fde2ebf · fde2ebf
1 parent 3303ab6
commit fde2ebf
Showing 1 changed file with 5 additions and 5 deletions.
diff --git a/Duper/Saturate.lean b/Duper/Saturate.lean
@@ -38,6 +38,11 @@ import Duper.Rules.FluidBoolHoist
 -- Type inhabitation reasoning rules
 import Duper.Util.TypeInhabitationReasoning
 
+register_option duper.maxSaturationTime : Nat := {
+  defValue := 500
+  descr := "Time limit for saturation procedure, in s"
+}
+
 namespace Duper
 
 namespace ProverM
@@ -54,11 +59,6 @@ initialize
   registerTraceClass `duper.timeout.debug.fullPassiveSet
   registerTraceClass `duper.misc.debug
 
-register_option duper.maxSaturationTime : Nat := {
-  defValue := 500
-  descr := "Time limit for saturation procedure, in s"
-}
-
 def getMaxSaturationTime (opts : Options) : Nat :=
   duper.maxSaturationTime.get opts * 1000