From 25b262d218f1f439a24a4db7dc3389f6a9884324 Mon Sep 17 00:00:00 2001 From: pottier Date: Fri, 25 Jun 2010 13:57:31 +0000 Subject: 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 --- plugins/nsatz/NsatzR.v | 1 + 1 file changed, 1 insertion(+) (limited to 'plugins/nsatz') 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) ; -- cgit v1.2.3