mirror of
https://github.com/microsoft/regorus.git
synced 2026-08-05 02:16:11 +00:00
Avoid some build errors
This commit is contained in:
@@ -13,8 +13,6 @@ use alloc::collections::{BTreeMap, BTreeSet};
|
||||
|
||||
use anyhow::{bail, Result};
|
||||
|
||||
use vstd::prelude::*;
|
||||
|
||||
#[inline]
|
||||
pub fn enforce_limit() -> Result<()> {
|
||||
crate::utils::limits::check_memory_limit_if_needed().map_err(anyhow::Error::new)
|
||||
|
||||
@@ -28,14 +28,17 @@ use serde::ser::Serializer;
|
||||
use serde::Serialize;
|
||||
|
||||
use vstd::prelude::*;
|
||||
#[cfg(verus_keep_ghost)]
|
||||
use vstd::float::*;
|
||||
#[cfg(verus_keep_ghost)]
|
||||
use vstd::std_specs::convert::*;
|
||||
#[cfg(verus_keep_ghost)]
|
||||
use vstd::std_specs::cmp::*;
|
||||
|
||||
use crate::*;
|
||||
|
||||
use crate::verusspec::bigint::*;
|
||||
use crate::verusspec::float::*;
|
||||
use crate::verusspec::utils::*;
|
||||
|
||||
verus! {
|
||||
|
||||
|
||||
Reference in New Issue
Block a user