diff options
| -rw-r--r-- | plugins/nsatz/NsatzR.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/nsatz/NsatzR.v b/plugins/nsatz/NsatzR.v index 0664a3f78..5db25599c 100644 --- a/plugins/nsatz/NsatzR.v +++ b/plugins/nsatz/NsatzR.v @@ -363,6 +363,7 @@ Ltac nsatzR_gen radicalmax info lparam lvar n RNG lH _rl := let SplitPolyList kont := match lpol with | ?p2::?lp2 => kont p2 lp2 + | _ => idtac "polynomial not in the ideal" end in SplitPolyList ltac:(fun p lp => set (p21:=p) ; |