bug 2328 fixed: failure when polynomial not i ideal

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13195 85f007b7-540e-0410-9357-904b9bb8a0f7

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) ;