[][src]Constant antic::NMOD_POLY_HGCD_CUTOFF

pub const NMOD_POLY_HGCD_CUTOFF: u32 = 100;