diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy index d98dcd0b..d8193a07 100644 --- a/src/Collections/Sequences/Seq.dfy +++ b/src/Collections/Sequences/Seq.dfy @@ -23,7 +23,7 @@ module {:options "-functionSyntax:4"} Seq { import opened Wrappers import opened MergeSort import opened Relations - import Math + import Dafny.Math /********************************************************** * diff --git a/src/JSON/Serializer.dfy b/src/JSON/Serializer.dfy index 1f936deb..37c3dee9 100644 --- a/src/JSON/Serializer.dfy +++ b/src/JSON/Serializer.dfy @@ -20,7 +20,7 @@ include "Spec.dfy" module {:options "-functionSyntax:4"} JSON.Serializer { import Seq - import Math + import Dafny.Math import opened Wrappers import opened BoundedInts import opened Utils.Str diff --git a/src/Math.dfy b/src/Math.dfy index 17cf15f2..89890128 100644 --- a/src/Math.dfy +++ b/src/Math.dfy @@ -5,7 +5,7 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -module {:options "-functionSyntax:4"} Math { +module {:options "-functionSyntax:4"} Dafny.Math { function Min(a: int, b: int): int { if a < b