diff options
| author | pottier | 2010-07-08 13:15:07 +0000 |
|---|---|---|
| committer | pottier | 2010-07-08 13:15:07 +0000 |
| commit | d9c825b5b5925be962d8d8d38a8534997f30a97b (patch) | |
| tree | c620a67749fbaf5c1857b4b265b7d4a67deb79fc /plugins/nsatz/NsatzR.v | |
| parent | 74bb3f23674caff6902665fde0c4608e28ff0877 (diff) | |
nsatz in an integral domain with specialization to Z and R
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13265 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/nsatz/NsatzR.v')
| -rw-r--r-- | plugins/nsatz/NsatzR.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/nsatz/NsatzR.v b/plugins/nsatz/NsatzR.v index 5db25599cc..004840ab31 100644 --- a/plugins/nsatz/NsatzR.v +++ b/plugins/nsatz/NsatzR.v @@ -352,8 +352,8 @@ Ltac nsatzR_gen radicalmax info lparam lvar n RNG lH _rl := (*idtac "variables:";idtac fv;*) let nparam := eval compute in (Z_of_nat (List.length lparam)) in let fv := parametres_en_tete fv lparam in - (* idtac "variables:"; idtac fv; - idtac "nparam:"; idtac nparam;*) + idtac "variables:"; idtac fv; + (* idtac "nparam:"; idtac nparam;*) let lpol := list_fold_right ltac:(fun p l => let p' := mkPol p fv in constr:(p'::l)) (@nil (PExpr Z)) |